src/Pure/ML/ml_antiquote.ML
changeset 35539 afa8cf9e63d8
parent 35401 bfcbab8592ba
child 35677 3007b46c1660
     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 *)