src/Pure/Isar/class.ML
changeset 40627 becf5d5187cc
parent 39557 fe5722fce758
child 41270 dea60d052923
     1.1 --- a/src/Pure/Isar/class.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -477,7 +477,7 @@
     1.4          --| junk))
     1.5        ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
     1.6    in
     1.7 -    explode #> scan_valids #> implode
     1.8 +    raw_explode #> scan_valids #> implode
     1.9    end;
    1.10  
    1.11  val type_name = sanitize_name o Long_Name.base_name;