changeset 2574 | 50da1be9a7e5 |
parent 2476 | 8f8652a8107f |
child 2595 | 07f775729e90 |
--- a/Nominal/nominal_dt_quot.ML Sun Nov 21 02:17:19 2010 +0000 +++ b/Nominal/nominal_dt_quot.ML Mon Nov 22 16:14:47 2010 +0900 @@ -99,7 +99,7 @@ val parser = Scan.repeat (exclude || any) in fun unraw_str s = - s |> explode + s |> raw_explode |> Scan.finite Symbol.stopper parser >> implode |> fst end