diff --git a/prelude/strings.v b/prelude/strings.v
index acf0c2c462ea8bf1699d2fa9488baf9bf3efdea1..3064d39d8402d6db524d2a1df4788b566a123567 100644
--- a/prelude/strings.v
+++ b/prelude/strings.v
@@ -31,11 +31,17 @@ Fixpoint string_rev_app (s1 s2 : string) : string :=
 Definition string_rev (s : string) : string := string_rev_app s "".
 
 (* Break a string up into lists of words, delimited by white space *)
+Definition is_space (x : Ascii.ascii) : bool :=
+  match x with
+  | "009" | "010" | "011" | "012" | "013" | " " => true | _ => false
+  end%char.
+
 Fixpoint words_go (cur : option string) (s : string) : list string :=
   match s with
   | "" => option_list (string_rev <$> cur)
-  | String " " s => option_list (string_rev <$> cur) ++ words_go None s
-  | String a s => words_go (Some (default (String a "") cur (String a))) s
+  | String a s =>
+     if is_space a then option_list (string_rev <$> cur) ++ words_go None s
+     else words_go (Some (default (String a "") cur (String a))) s
   end.
 Definition words : string → list string := words_go None.
 
diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
index bbb58d62aee652748fb81cdc917a3f2dde76d4bd..b999e0be35c707352b0efd322483188bc5218511 100644
--- a/proofmode/intro_patterns.v
+++ b/proofmode/intro_patterns.v
@@ -54,7 +54,6 @@ Fixpoint cons_name (kn : string) (k : list token) : list token :=
 Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   match s with
   | "" => rev (cons_name kn k)
-  | String " " s => tokenize_go s (cons_name kn k) ""
   | String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
   | String "_" s => tokenize_go s (TDrop :: cons_name kn k) ""
   | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
@@ -75,7 +74,9 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
   | String "*" (String "*" s) => tokenize_go s (TAll :: cons_name kn k) ""
   | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
-  | String a s => tokenize_go s k (String a kn)
+  | String a s =>
+     if is_space a then tokenize_go s (cons_name kn k) ""
+     else tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
 
diff --git a/proofmode/sel_patterns.v b/proofmode/sel_patterns.v
index 75aa2ee4934497054f859ca2bbe0a76131f40d69..4a77f4f08c3542f829382d95ea41e3038e70a7a7 100644
--- a/proofmode/sel_patterns.v
+++ b/proofmode/sel_patterns.v
@@ -20,14 +20,15 @@ Fixpoint cons_name (kn : string) (k : list sel_pat) : list sel_pat :=
 Fixpoint parse_go (s : string) (k : list sel_pat) (kn : string) : list sel_pat :=
   match s with
   | "" => rev (cons_name kn k)
-  | String " " s => parse_go s (cons_name kn k) ""
   | String "%" s => parse_go s (SelPure :: cons_name kn k) ""
   | String "#" s => parse_go s (SelPersistent :: cons_name kn k) ""
   | String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
       (String (Ascii.Ascii false false false true false false false true)
       (String (Ascii.Ascii true true true false true false false true) s)) =>
      parse_go s (SelSpatial :: cons_name kn k) ""
-  | String a s => parse_go s k (String a kn)
+  | String a s =>
+     if is_space a then parse_go s (cons_name kn k) ""
+     else parse_go s k (String a kn)
   end.
 Definition parse (s : string) : list sel_pat := parse_go s [] "".
 
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index 4f9cbada3d365104c34c3ad1cd5ab57fb390e2ad..25c548311febf7f7caf3c777c6c70ef1818de7e1 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -31,7 +31,6 @@ Fixpoint cons_name (kn : string) (k : list token) : list token :=
 Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   match s with
   | "" => rev (cons_name kn k)
-  | String " " s => tokenize_go s (cons_name kn k) ""
   | String "-" s => tokenize_go s (TMinus :: cons_name kn k) ""
   | String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
   | String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
@@ -40,7 +39,9 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
   | String ">" s => tokenize_go s (TModal :: cons_name kn k) ""
   | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
-  | String a s => tokenize_go s k (String a kn)
+  | String a s =>
+     if is_space a then tokenize_go s (cons_name kn k) ""
+     else tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".