src/Tools/code/code_target.ML
changeset 25985 8d69087f6a4b
parent 25969 d3f8ab2726ed
child 26010 a741416574e1
     1.1 --- a/src/Tools/code/code_target.ML	Sat Jan 26 17:08:43 2008 +0100
     1.2 +++ b/src/Tools/code/code_target.ML	Sat Jan 26 20:01:37 2008 +0100
     1.3 @@ -2132,7 +2132,7 @@
     1.4    OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
     1.5      parse_multi_syntax P.xname
     1.6        (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
     1.7 -        (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) []))
     1.8 +        (P.term --| (P.$$$ "\<equiv>" || P.$$$ "==") -- P.string)) []))
     1.9      >> (Toplevel.theory oo fold) (fn (target, syns) =>
    1.10            fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
    1.11    );