changeset 2582 | 6c4372a1f220 |
parent 2574 | 50da1be9a7e5 |
child 2595 | 07f775729e90 |
--- a/Nominal/nominal_dt_quot.ML Wed Nov 24 02:36:21 2010 +0000 +++ b/Nominal/nominal_dt_quot.ML Thu Nov 25 01:18:24 2010 +0000 @@ -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