equal
deleted
inserted
replaced
97 val exclude = |
97 val exclude = |
98 Scan.repeat (Scan.unless raw any) --| raw >> implode |
98 Scan.repeat (Scan.unless raw any) --| raw >> implode |
99 val parser = Scan.repeat (exclude || any) |
99 val parser = Scan.repeat (exclude || any) |
100 in |
100 in |
101 fun unraw_str s = |
101 fun unraw_str s = |
102 s |> explode |
102 s |> raw_explode |
103 |> Scan.finite Symbol.stopper parser >> implode |
103 |> Scan.finite Symbol.stopper parser >> implode |
104 |> fst |
104 |> fst |
105 end |
105 end |
106 |
106 |
107 fun unraw_vars_thm thm = |
107 fun unraw_vars_thm thm = |