1.1 --- a/src/Pure/ML/ml_antiquote.ML Wed Mar 03 00:00:44 2010 +0100
1.2 +++ b/src/Pure/ML/ml_antiquote.ML Wed Mar 03 00:28:22 2010 +0100
1.3 @@ -104,7 +104,7 @@
1.4
1.5 fun class syn = Args.theory -- Scan.lift Args.name_source >> (fn (thy, s) =>
1.6 Sign.read_class thy s
1.7 - |> syn ? Long_Name.base_name (* FIXME authentic syntax *)
1.8 + |> syn ? Syntax.mark_class
1.9 |> ML_Syntax.print_string);
1.10
1.11 val _ = inline "class" (class false);
1.12 @@ -130,7 +130,7 @@
1.13 val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
1.14 val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
1.15 val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
1.16 -val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Long_Name.base_name c)); (* FIXME authentic syntax *)
1.17 +val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Syntax.mark_type c));
1.18
1.19
1.20 (* constants *)