# HG changeset patch
# User wenzelm
# Date 1267572502 -3600
# Node ID afa8cf9e63d84e0c08b2b48ddda8f92ce23aab23
# Parent  bd7d6f65976ed7bfa807aacd4b46b14d00046058
authentic syntax for classes and type constructors;
read/intern formal entities just after raw parsing, extern just before final pretty printing;
discontinued _class token translation;
moved Local_Syntax.extern_term to Syntax/printer.ML;
misc tuning;

diff -r bd7d6f65976e -r afa8cf9e63d8 src/Pure/Isar/local_syntax.ML
--- a/src/Pure/Isar/local_syntax.ML	Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Isar/local_syntax.ML	Wed Mar 03 00:28:22 2010 +0100
@@ -4,13 +4,11 @@
 Local syntax depending on theory syntax.
 *)
 
-val show_structs = Unsynchronized.ref false;
-
 signature LOCAL_SYNTAX =
 sig
   type T
   val syn_of: T -> Syntax.syntax
-  val structs_of: T -> string list
+  val idents_of: T -> {structs: string list, fixes: string list}
   val init: theory -> T
   val rebuild: theory -> T -> T
   datatype kind = Type | Const | Fixed
@@ -19,7 +17,6 @@
   val restore_mode: T -> T -> T
   val update_modesyntax: theory -> bool -> Syntax.mode ->
     (kind * (string * typ * mixfix)) list -> T -> T
-  val extern_term: T -> term -> term
 end;
 
 structure Local_Syntax: LOCAL_SYNTAX =
@@ -49,8 +46,7 @@
   Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
 
 fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
-fun idents_of (Syntax {idents, ...}) = idents;
-val structs_of = #1 o idents_of;
+fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
 
 
 (* build syntax *)
@@ -125,21 +121,4 @@
 fun update_modesyntax thy add mode args syntax =
   syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
 
-
-(* extern_term *)
-
-fun extern_term syntax =
-  let
-    val (structs, fixes) = idents_of syntax;
-    fun map_free (t as Free (x, T)) =
-          let val i = find_index (fn s => s = x) structs + 1 in
-            if i = 0 andalso member (op =) fixes x then
-              Term.Const (Syntax.mark_fixed x, T)
-            else if i = 1 andalso not (! show_structs) then
-              Syntax.const "_struct" $ Syntax.const "_indexdefault"
-            else t
-          end
-      | map_free t = t;
-  in Term.map_aterms map_free end;
-
 end;
diff -r bd7d6f65976e -r afa8cf9e63d8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 03 00:28:22 2010 +0100
@@ -363,15 +363,11 @@
           (Pretty.str (setmp_CRITICAL show_question_marks true Term.string_of_vname (x', i))))
   | NONE => Pretty.mark Markup.var (Pretty.str s));
 
-fun class_markup _ c =    (* FIXME authentic syntax *)
-  Pretty.mark (Markup.tclassN, []) (Pretty.str c);
-
 fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
 
 val token_trans =
  Syntax.tokentrans_mode ""
-  [("class", class_markup),
-   ("tfree", plain_markup Markup.tfree),
+  [("tfree", plain_markup Markup.tfree),
    ("tvar", plain_markup Markup.tvar),
    ("free", free_or_skolem),
    ("bound", plain_markup Markup.bound),
@@ -601,14 +597,12 @@
    {get_sort = get_sort thy (Variable.def_sort ctxt),
     map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
       handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
-    map_free = intern_skolem ctxt (Variable.def_type ctxt false),
-    map_type = Sign.intern_tycons thy,
-    map_sort = Sign.intern_sort thy}
+    map_free = intern_skolem ctxt (Variable.def_type ctxt false)}
   end;
 
 fun decode_term ctxt =
-  let val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt
-  in Syntax.decode_term get_sort map_const map_free map_type map_sort end;
+  let val {get_sort, map_const, map_free} = term_context ctxt
+  in Syntax.decode_term get_sort map_const map_free end;
 
 end;
 
@@ -677,26 +671,23 @@
 fun parse_sort ctxt text =
   let
     val (syms, pos) = Syntax.parse_token Markup.sort text;
-    val S = Syntax.standard_parse_sort ctxt (syn_of ctxt)
-        (Sign.intern_sort (theory_of ctxt)) (syms, pos)
+    val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
       handle ERROR msg => cat_error msg  ("Failed to parse sort" ^ Position.str_of pos)
   in S end;
 
 fun parse_typ ctxt text =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = theory_of ctxt;
     val get_sort = get_sort thy (Variable.def_sort ctxt);
-
     val (syms, pos) = Syntax.parse_token Markup.typ text;
-    val T = Sign.intern_tycons thy
-        (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) (syms, pos))
-      handle ERROR msg => cat_error msg  ("Failed to parse type" ^ Position.str_of pos);
+    val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (syms, pos)
+      handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
   in T end;
 
 fun parse_term T ctxt text =
   let
     val thy = theory_of ctxt;
-    val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
+    val {get_sort, map_const, map_free} = term_context ctxt;
 
     val (T', _) = TypeInfer.paramify_dummies T 0;
     val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
@@ -704,29 +695,35 @@
 
     fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
       handle ERROR msg => SOME msg;
-    val t = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
-        map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
+    val t =
+      Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
+        ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
       handle ERROR msg => cat_error msg  ("Failed to parse " ^ kind ^ Position.str_of pos);
   in t end;
 
 
-fun unparse_sort ctxt S =
-  Syntax.standard_unparse_sort ctxt (syn_of ctxt) (Sign.extern_sort (theory_of ctxt) S);
+fun unparse_sort ctxt =
+  Syntax.standard_unparse_sort {extern_class = Sign.extern_class (theory_of ctxt)}
+    ctxt (syn_of ctxt);
 
-fun unparse_typ ctxt T =
-  Syntax.standard_unparse_typ ctxt (syn_of ctxt) (Sign.extern_typ (theory_of ctxt) T);
+fun unparse_typ ctxt =
+  let
+    val thy = theory_of ctxt;
+    val extern = {extern_class = Sign.extern_class thy, extern_type = Sign.extern_type thy};
+  in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end;
 
-fun unparse_term ctxt t =
+fun unparse_term ctxt =
   let
     val thy = theory_of ctxt;
     val syntax = syntax_of ctxt;
     val consts = consts_of ctxt;
+    val extern =
+     {extern_class = Sign.extern_class thy,
+      extern_type = Sign.extern_type thy,
+      extern_const = Consts.extern consts};
   in
-    t
-    |> Sign.extern_term thy
-    |> Local_Syntax.extern_term syntax
-    |> Syntax.standard_unparse_term (Consts.extern consts) ctxt
-        (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
+    Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
+      (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
   end;
 
 in
@@ -1010,18 +1007,20 @@
       in Syntax.Constant d end
   | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
 
+val typ = Simple_Syntax.read_typ;
+
 in
 
 val _ = Context.>> (Context.map_theory
- (Sign.add_syntax
-   [("_context_const", "id => logic", Delimfix "CONST _"),
-    ("_context_const", "id => aprop", Delimfix "CONST _"),
-    ("_context_const", "longid => logic", Delimfix "CONST _"),
-    ("_context_const", "longid => aprop", Delimfix "CONST _"),
-    ("_context_xconst", "id => logic", Delimfix "XCONST _"),
-    ("_context_xconst", "id => aprop", Delimfix "XCONST _"),
-    ("_context_xconst", "longid => logic", Delimfix "XCONST _"),
-    ("_context_xconst", "longid => aprop", Delimfix "XCONST _")] #>
+ (Sign.add_syntax_i
+   [("_context_const", typ "id => logic", Delimfix "CONST _"),
+    ("_context_const", typ "id => aprop", Delimfix "CONST _"),
+    ("_context_const", typ "longid => logic", Delimfix "CONST _"),
+    ("_context_const", typ "longid => aprop", Delimfix "CONST _"),
+    ("_context_xconst", typ "id => logic", Delimfix "XCONST _"),
+    ("_context_xconst", typ "id => aprop", Delimfix "XCONST _"),
+    ("_context_xconst", typ "longid => logic", Delimfix "XCONST _"),
+    ("_context_xconst", typ "longid => aprop", Delimfix "XCONST _")] #>
   Sign.add_advanced_trfuns
     ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
 
@@ -1032,8 +1031,8 @@
 
 local
 
-fun type_syntax (Type (c, args), mx) =  (* FIXME authentic syntax *)
-      SOME (Local_Syntax.Type, (Long_Name.base_name c, Syntax.make_type (length args), mx))
+fun type_syntax (Type (c, args), mx) =
+      SOME (Local_Syntax.Type, (Syntax.mark_type c, Syntax.make_type (length args), mx))
   | type_syntax _ = NONE;
 
 fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
@@ -1345,7 +1344,7 @@
       val prt_term = Syntax.pretty_term ctxt;
 
       (*structures*)
-      val structs = Local_Syntax.structs_of (syntax_of ctxt);
+      val {structs, ...} = Local_Syntax.idents_of (syntax_of ctxt);
       val prt_structs =
         if null structs then []
         else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
@@ -1415,3 +1414,4 @@
   end;
 
 end;
+
diff -r bd7d6f65976e -r afa8cf9e63d8 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Mar 03 00:28:22 2010 +0100
@@ -104,7 +104,7 @@
 
 fun class syn = Args.theory -- Scan.lift Args.name_source >> (fn (thy, s) =>
   Sign.read_class thy s
-  |> syn ? Long_Name.base_name   (* FIXME authentic syntax *)
+  |> syn ? Syntax.mark_class
   |> ML_Syntax.print_string);
 
 val _ = inline "class" (class false);
@@ -130,7 +130,7 @@
 val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
 val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
 val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
-val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Long_Name.base_name c));  (* FIXME authentic syntax *)
+val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Syntax.mark_type c));
 
 
 (* constants *)
diff -r bd7d6f65976e -r afa8cf9e63d8 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Syntax/printer.ML	Wed Mar 03 00:28:22 2010 +0100
@@ -11,29 +11,32 @@
   val show_types: bool Unsynchronized.ref
   val show_no_free_types: bool Unsynchronized.ref
   val show_all_types: bool Unsynchronized.ref
+  val show_structs: bool Unsynchronized.ref
   val pp_show_brackets: Pretty.pp -> Pretty.pp
 end;
 
 signature PRINTER =
 sig
   include PRINTER0
-  val term_to_ast: Proof.context ->
-    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
+  val sort_to_ast: Proof.context ->
+    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
   val typ_to_ast: Proof.context ->
     (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
-  val sort_to_ast: Proof.context ->
-    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
+  val term_to_ast: {structs: string list, fixes: string list} -> string list -> Proof.context ->
+    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
   type prtabs
   val empty_prtabs: prtabs
   val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
   val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
   val merge_prtabs: prtabs -> prtabs -> prtabs
-  val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
-    -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
-    -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
-  val pretty_typ_ast: Proof.context -> bool -> prtabs
-    -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
-    -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
+  val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring,
+      extern_const: string -> xstring} -> Proof.context -> bool -> prtabs ->
+    (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+    (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
+  val pretty_typ_ast: {extern_class: string -> xstring, extern_type: string -> xstring} ->
+    Proof.context -> bool -> prtabs ->
+    (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+    (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
 end;
 
 structure Printer: PRINTER =
@@ -47,6 +50,7 @@
 val show_brackets = Unsynchronized.ref false;
 val show_no_free_types = Unsynchronized.ref false;
 val show_all_types = Unsynchronized.ref false;
+val show_structs = Unsynchronized.ref false;
 
 fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
   Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
@@ -84,8 +88,7 @@
 
 fun ast_of_termT ctxt trf tm =
   let
-    fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
-      | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
+    fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
       | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
       | ast_of (Const (a, _)) = trans a []
       | ast_of (t as _ $ _) =
@@ -105,19 +108,30 @@
 
 (** term_to_ast **)
 
-fun mark_freevars ((t as Const (c, _)) $ u) =
-      if member (op =) SynExt.standard_token_markers c then (t $ u)
-      else t $ mark_freevars u
-  | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
-  | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
-  | mark_freevars (t as Free _) = Lexicon.const "_free" $ t
-  | mark_freevars (t as Var (xi, T)) =
-      if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
-      else Lexicon.const "_var" $ t
-  | mark_freevars a = a;
+fun ast_of_term idents consts ctxt trf
+    show_all_types no_freeTs show_types show_sorts show_structs tm =
+  let
+    val {structs, fixes} = idents;
 
-fun ast_of_term ctxt trf show_all_types no_freeTs show_types show_sorts tm =
-  let
+    fun mark_atoms ((t as Const (c, T)) $ u) =
+          if member (op =) consts c then (t $ u)
+          else Const (Lexicon.mark_const c, T) $ mark_atoms u
+      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
+      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
+      | mark_atoms (Const (c, T)) = Const (Lexicon.mark_const c, T)
+      | mark_atoms (t as Free (x, T)) =
+          let val i = find_index (fn s => s = x) structs + 1 in
+            if i = 0 andalso member (op =) fixes x then
+              Term.Const (Lexicon.mark_fixed x, T)
+            else if i = 1 andalso not show_structs then
+              Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
+            else Lexicon.const "_free" $ t
+          end
+      | mark_atoms (t as Var (xi, T)) =
+          if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
+          else Lexicon.const "_var" $ t
+      | mark_atoms a = a;
+
     fun prune_typs (t_seen as (Const _, _)) = t_seen
       | prune_typs (t as Free (x, ty), seen) =
           if ty = dummyT then (t, seen)
@@ -148,9 +162,9 @@
           Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
       | (Const ("_idtdummy", T), ts) =>
           Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
-      | (c' as Const (c, T), ts) =>
+      | (const as Const (c, T), ts) =>
           if show_all_types
-          then Ast.mk_appl (constrain c' T) (map ast_of ts)
+          then Ast.mk_appl (constrain const T) (map ast_of ts)
           else trans c T ts
       | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
 
@@ -162,18 +176,18 @@
       if show_types andalso T <> dummyT then
         Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
           ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
-      else simple_ast_of t
+      else simple_ast_of t;
   in
     tm
     |> SynTrans.prop_tr'
-    |> (if show_types then #1 o prune_typs o rpair [] else I)
-    |> mark_freevars
+    |> show_types ? (#1 o prune_typs o rpair [])
+    |> mark_atoms
     |> ast_of
   end;
 
-fun term_to_ast ctxt trf tm =
-  ast_of_term ctxt trf (! show_all_types) (! show_no_free_types)
-    (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
+fun term_to_ast idents consts ctxt trf tm =
+  ast_of_term idents consts ctxt trf (! show_all_types) (! show_no_free_types)
+    (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;
 
 
 
@@ -267,8 +281,10 @@
   | is_chain [Arg _] = true
   | is_chain _  = false;
 
-fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
+fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 p0 =
   let
+    val {extern_class, extern_type, extern_const} = extern;
+
     fun token_trans a x =
       (case tokentrf a of
         NONE =>
@@ -291,7 +307,7 @@
             val (Ts, args') = synT markup (symbs, args);
           in
             if type_mode then (astT (t, p) @ Ts, args')
-            else (pretty I ctxt tabs trf tokentrf true curried t p @ Ts, args')
+            else (pretty extern ctxt tabs trf tokentrf true curried t p @ Ts, args')
           end
       | synT markup (String s :: symbs, args) =
           let val (Ts, args') = synT markup (symbs, args);
@@ -312,7 +328,6 @@
             val (Ts, args') = synT markup (symbs, args);
             val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
           in (T :: Ts, args') end
-      | synT _ (_ :: _, []) = sys_error "synT"
 
     and parT markup (pr, args, p, p': int) = #1 (synT markup
           (if p > p' orelse
@@ -320,13 +335,12 @@
             then [Block (1, Space "(" :: pr @ [Space ")"])]
             else pr, args))
 
-    and atomT a =
-      (case try Lexicon.unmark_const a of
-        SOME c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c))
-      | NONE =>
-          (case try Lexicon.unmark_fixed a of
-            SOME x => the (token_trans "_free" x)
-          | NONE => Pretty.str a))
+    and atomT a = a |> Lexicon.unmark
+     {case_class = fn c => Pretty.mark (Markup.tclass c) (Pretty.str (extern_class c)),
+      case_type = fn c => Pretty.mark (Markup.tycon c) (Pretty.str (extern_type c)),
+      case_const = fn c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c)),
+      case_fixed = fn x => the (token_trans "_free" x),
+      case_default = Pretty.str}
 
     and prefixT (_, a, [], _) = [atomT a]
       | prefixT (c, _, args, p) = astT (appT (c, args), p)
@@ -334,15 +348,16 @@
     and splitT 0 ([x], ys) = (x, ys)
       | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
       | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
-      | splitT _ _ = sys_error "splitT"
 
     and combT (tup as (c, a, args, p)) =
       let
         val nargs = length args;
-        val markup = Pretty.mark
-          (Markup.const (Lexicon.unmark_const a) handle Fail _ =>
-            (Markup.fixed (Lexicon.unmark_fixed a)))
-          handle Fail _ => I;
+        val markup = a |> Lexicon.unmark
+         {case_class = Pretty.mark o Markup.tclass,
+          case_type = Pretty.mark o Markup.tycon,
+          case_const = Pretty.mark o Markup.const,
+          case_fixed = Pretty.mark o Markup.fixed,
+          case_default = K I};
 
         (*find matching table entry, or print as prefix / postfix*)
         fun prnt ([], []) = prefixT tup
@@ -371,15 +386,16 @@
 
 (* pretty_term_ast *)
 
-fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
-  pretty extern_const ctxt (mode_tabs prtabs (print_mode_value ()))
+fun pretty_term_ast extern ctxt curried prtabs trf tokentrf ast =
+  pretty extern ctxt (mode_tabs prtabs (print_mode_value ()))
     trf tokentrf false curried ast 0;
 
 
 (* pretty_typ_ast *)
 
-fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
-  pretty I ctxt (mode_tabs prtabs (print_mode_value ()))
+fun pretty_typ_ast {extern_class, extern_type} ctxt _ prtabs trf tokentrf ast =
+  pretty {extern_class = extern_class, extern_type = extern_type, extern_const = I}
+    ctxt (mode_tabs prtabs (print_mode_value ()))
     trf tokentrf true false ast 0;
 
 end;
diff -r bd7d6f65976e -r afa8cf9e63d8 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Mar 03 00:28:22 2010 +0100
@@ -282,7 +282,8 @@
       if not (exists is_index args) then (const, typ, [])
       else
         let
-          val indexed_const = if const <> "" then "_indexed_" ^ const
+          val indexed_const =
+            if const <> "" then const ^ "_indexed"
             else err_in_mfix "Missing constant name for indexed syntax" mfix;
           val rangeT = Term.range_type typ handle Match =>
             err_in_mfix "Missing structure argument for indexed syntax" mfix;
@@ -387,7 +388,7 @@
 fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
 
 val standard_token_classes =
-  ["class", "tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
+  ["tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
 
 val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
 
diff -r bd7d6f65976e -r afa8cf9e63d8 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Mar 03 00:28:22 2010 +0100
@@ -34,16 +34,16 @@
   val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
   val constrainAbsC: string
   val pure_trfuns:
-      (string * (Ast.ast list -> Ast.ast)) list *
-      (string * (term list -> term)) list *
-      (string * (term list -> term)) list *
-      (string * (Ast.ast list -> Ast.ast)) list
+    (string * (Ast.ast list -> Ast.ast)) list *
+    (string * (term list -> term)) list *
+    (string * (term list -> term)) list *
+    (string * (Ast.ast list -> Ast.ast)) list
   val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
   val struct_trfuns: string list ->
-      (string * (Ast.ast list -> Ast.ast)) list *
-      (string * (term list -> term)) list *
-      (string * (bool -> typ -> term list -> term)) list *
-      (string * (Ast.ast list -> Ast.ast)) list
+    (string * (Ast.ast list -> Ast.ast)) list *
+    (string * (term list -> term)) list *
+    (string * (bool -> typ -> term list -> term)) list *
+    (string * (Ast.ast list -> Ast.ast)) list
 end;
 
 signature SYN_TRANS =
@@ -131,7 +131,7 @@
 
 fun mk_type ty =
   Lexicon.const "_constrain" $
-    Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "itself" $ ty);
+    Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
 
 fun ofclass_tr (*"_ofclass"*) [ty, cls] = cls $ mk_type ty
   | ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts);
@@ -143,7 +143,7 @@
 
 (* meta propositions *)
 
-fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "prop"
+fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
   | aprop_tr (*"_aprop"*) ts = raise TERM ("aprop_tr", ts);
 
 
@@ -195,7 +195,8 @@
 fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
   | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
   | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
-      list_comb (c $ update_name_tr [t] $ (Lexicon.const "fun" $ ty $ Lexicon.const "dummy"), ts)
+      list_comb (c $ update_name_tr [t] $
+        (Lexicon.const "\\<^type>fun" $ ty $ Lexicon.const "\\<^type>dummy"), ts)
   | update_name_tr ts = raise TERM ("update_name_tr", ts);
 
 
@@ -368,7 +369,7 @@
     fun is_prop Ts t =
       fastype_of1 (Ts, t) = propT handle TERM _ => false;
 
-    fun is_term (Const ("\\<^const>Pure.term", _) $ _) = true
+    fun is_term (Const ("Pure.term", _) $ _) = true
       | is_term _ = false;
 
     fun tr' _ (t as Const _) = t
@@ -381,7 +382,7 @@
       | tr' Ts (t as Bound _) =
           if is_prop Ts t then aprop t else t
       | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
-      | tr' Ts (t as t1 $ (t2 as Const ("\\<^const>TYPE", Type ("itself", [T])))) =
+      | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
           if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
           else tr' Ts t1 $ tr' Ts t2
       | tr' Ts (t as t1 $ t2) =
@@ -568,7 +569,7 @@
 
     val free_fixed = Term.map_aterms
       (fn t as Const (c, T) =>
-          (case try (unprefix Lexicon.fixedN) c of
+          (case try Lexicon.unmark_fixed c of
             NONE => t
           | SOME x => Free (x, T))
         | t => t);
diff -r bd7d6f65976e -r afa8cf9e63d8 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Mar 03 00:28:22 2010 +0100
@@ -29,7 +29,10 @@
   val mode_default: mode
   val mode_input: mode
   val merge_syntaxes: syntax -> syntax -> syntax
-  val basic_syn: syntax
+  val empty_syntax: syntax
+  val basic_syntax:
+   {read_class: theory -> xstring -> string,
+    read_type: theory -> xstring -> string} -> syntax
   val basic_nonterms: string list
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
@@ -41,25 +44,24 @@
   val ambiguity_limit: int Unsynchronized.ref
   val standard_parse_term: Pretty.pp -> (term -> string option) ->
     (((string * int) * sort) list -> string * int -> Term.sort) ->
-    (string -> bool * string) -> (string -> string option) ->
-    (typ -> typ) -> (sort -> sort) -> Proof.context ->
+    (string -> bool * string) -> (string -> string option) -> Proof.context ->
     (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
   val standard_parse_typ: Proof.context -> syntax ->
-    ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
-    Symbol_Pos.T list * Position.T -> typ
-  val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) ->
-    Symbol_Pos.T list * Position.T -> sort
+    ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
+  val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
   datatype 'a trrule =
     ParseRule of 'a * 'a |
     PrintRule of 'a * 'a |
     ParsePrintRule of 'a * 'a
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   val is_const: syntax -> string -> bool
-  val standard_unparse_term: (string -> xstring) ->
-    Proof.context -> syntax -> bool -> term -> Pretty.T
-  val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
-  val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
-  val update_consts: string list -> syntax -> syntax
+  val standard_unparse_term: {structs: string list, fixes: string list} ->
+    {extern_class: string -> xstring, extern_type: string -> xstring,
+      extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
+  val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
+    Proof.context -> syntax -> typ -> Pretty.T
+  val standard_unparse_sort: {extern_class: string -> xstring} ->
+    Proof.context -> syntax -> sort -> Pretty.T
   val update_trfuns:
     (string * ((ast list -> ast) * stamp)) list *
     (string * ((term list -> term) * stamp)) list *
@@ -300,7 +302,7 @@
       lexicon =
         if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
       gram = if changed then Parser.extend_gram gram xprods else gram,
-      consts = Library.merge (op =) (consts1, filter_out (can Lexicon.unmark_const) consts2),
+      consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
       prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
       parse_ast_trtab =
         update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
@@ -381,9 +383,9 @@
 
 (* basic syntax *)
 
-val basic_syn =
+fun basic_syntax read =
   empty_syntax
-  |> update_syntax mode_default TypeExt.type_ext
+  |> update_syntax mode_default (TypeExt.type_ext read)
   |> update_syntax mode_default SynExt.pure_ext;
 
 val basic_nonterms =
@@ -547,26 +549,25 @@
             map (Pretty.string_of_term pp) (take limit results)))
       end;
 
-fun standard_parse_term pp check get_sort map_const map_free map_type map_sort
-    ctxt is_logtype syn ty (syms, pos) =
+fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
   read ctxt is_logtype syn ty (syms, pos)
-  |> map (TypeExt.decode_term get_sort map_const map_free map_type map_sort)
+  |> map (TypeExt.decode_term get_sort map_const map_free)
   |> disambig (Printer.pp_show_brackets pp) check;
 
 
 (* read types *)
 
-fun standard_parse_typ ctxt syn get_sort map_sort (syms, pos) =
+fun standard_parse_typ ctxt syn get_sort (syms, pos) =
   (case read ctxt (K false) syn SynExt.typeT (syms, pos) of
-    [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts map_sort t)) map_sort t
+    [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts t)) t
   | _ => error (ambiguity_msg pos));
 
 
 (* read sorts *)
 
-fun standard_parse_sort ctxt syn map_sort (syms, pos) =
+fun standard_parse_sort ctxt syn (syms, pos) =
   (case read ctxt (K false) syn TypeExt.sortT (syms, pos) of
-    [t] => TypeExt.sort_of_term map_sort t
+    [t] => TypeExt.sort_of_term t
   | _ => error (ambiguity_msg pos));
 
 
@@ -640,8 +641,8 @@
 
 fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
   let
-    val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
-    val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
+    val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
+    val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
   in
     Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
       (lookup_tokentr tokentrtab (print_mode_value ()))
@@ -650,14 +651,16 @@
 
 in
 
-fun standard_unparse_term extern =
-  unparse_t Printer.term_to_ast (Printer.pretty_term_ast extern) Markup.term;
+fun standard_unparse_term idents extern =
+  unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
 
-fun standard_unparse_typ ctxt syn =
-  unparse_t Printer.typ_to_ast Printer.pretty_typ_ast Markup.typ ctxt syn false;
+fun standard_unparse_typ extern ctxt syn =
+  unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
 
-fun standard_unparse_sort ctxt syn =
-  unparse_t Printer.sort_to_ast Printer.pretty_typ_ast Markup.sort ctxt syn false;
+fun standard_unparse_sort {extern_class} ctxt syn =
+  unparse_t (K Printer.sort_to_ast)
+    (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
+    Markup.sort ctxt syn false;
 
 end;
 
@@ -667,7 +670,6 @@
 
 fun ext_syntax f decls = update_syntax mode_default (f decls);
 
-val update_consts = ext_syntax SynExt.syn_ext_const_names;
 val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
 val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
 val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
diff -r bd7d6f65976e -r afa8cf9e63d8 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Wed Mar 03 00:28:22 2010 +0100
@@ -1,19 +1,17 @@
 (*  Title:      Pure/Syntax/type_ext.ML
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
-Utilities for input and output of types.  Also the concrete syntax of
-types, which is required to bootstrap Pure.
+Utilities for input and output of types.  The concrete syntax of types.
 *)
 
 signature TYPE_EXT0 =
 sig
-  val sort_of_term: (sort -> sort) -> term -> sort
-  val term_sorts: (sort -> sort) -> term -> (indexname * sort) list
-  val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
+  val sort_of_term: term -> sort
+  val term_sorts: term -> (indexname * sort) list
+  val typ_of_term: (indexname -> sort) -> term -> typ
   val type_constraint: typ -> term -> term
   val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
-    (string -> bool * string) -> (string -> string option) ->
-    (typ -> typ) -> (sort -> sort) -> term -> term
+    (string -> bool * string) -> (string -> string option) -> term -> term
   val term_of_typ: bool -> typ -> term
   val no_brackets: unit -> bool
   val no_type_brackets: unit -> bool
@@ -25,7 +23,9 @@
   val term_of_sort: sort -> term
   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val sortT: typ
-  val type_ext: SynExt.syn_ext
+  val type_ext:
+   {read_class: theory -> string -> string,
+    read_type: theory -> string -> string} -> SynExt.syn_ext
 end;
 
 structure TypeExt: TYPE_EXT =
@@ -35,30 +35,28 @@
 
 (* sort_of_term *)
 
-fun sort_of_term (map_sort: sort -> sort) tm =
+fun sort_of_term tm =
   let
-    fun classes (Const (c, _)) = [c]
-      | classes (Free (c, _)) = [c]
-      | classes (Const ("_class", _) $ Free (c, _)) = [c]
-      | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
-      | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
-      | classes (Const ("_classes", _) $ (Const ("_class", _) $ Free (c, _)) $ cs) = c :: classes cs
-      | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
+    fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
+
+    fun class s = Lexicon.unmark_class s handle Fail _ => err ();
+
+    fun classes (Const (s, _)) = [class s]
+      | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
+      | classes _ = err ();
 
     fun sort (Const ("_topsort", _)) = []
-      | sort (Const (c, _)) = [c]
-      | sort (Free (c, _)) = [c]
-      | sort (Const ("_class", _) $ Free (c, _)) = [c]
+      | sort (Const (s, _)) = [class s]
       | sort (Const ("_sort", _) $ cs) = classes cs
-      | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
-  in map_sort (sort tm) end;
+      | sort _ = err ();
+  in sort tm end;
 
 
 (* term_sorts *)
 
-fun term_sorts map_sort tm =
+fun term_sorts tm =
   let
-    val sort_of = sort_of_term map_sort;
+    val sort_of = sort_of_term;
 
     fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
           insert (op =) ((x, ~1), sort_of cs)
@@ -76,11 +74,11 @@
 
 (* typ_of_term *)
 
-fun typ_of_term get_sort map_sort t =
+fun typ_of_term get_sort tm =
   let
-    fun typ_of (Free (x, _)) =
-          if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
-          else Type (x, [])
+    fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
+
+    fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
       | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
       | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
       | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
@@ -90,17 +88,16 @@
       | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
       | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
           TVar (xi, get_sort xi)
-      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term map_sort t)
-      | typ_of tm =
+      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
+      | typ_of t =
           let
-            val (t, ts) = Term.strip_comb tm;
+            val (head, args) = Term.strip_comb t;
             val a =
-              (case t of
-                Const (x, _) => x
-              | Free (x, _) => x
-              | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
-          in Type (a, map typ_of ts) end;
-  in typ_of t end;
+              (case head of
+                Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
+              | _ => err ());
+          in Type (a, map typ_of args) end;
+  in typ_of tm end;
 
 
 (* decode_term -- transform parse tree into raw term *)
@@ -109,30 +106,30 @@
   if T = dummyT then t
   else Const ("_type_constraint_", T --> T) $ t;
 
-fun decode_term get_sort map_const map_free map_type map_sort tm =
+fun decode_term get_sort map_const map_free tm =
   let
-    val sort_env = term_sorts map_sort tm;
-    val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort;
+    val sort_env = term_sorts tm;
+    val decodeT = typ_of_term (get_sort sort_env);
 
     fun decode (Const ("_constrain", _) $ t $ typ) =
           type_constraint (decodeT typ) (decode t)
       | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
           if T = dummyT then Abs (x, decodeT typ, decode t)
-          else type_constraint (decodeT typ --> dummyT) (Abs (x, map_type T, decode t))
-      | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t)
+          else type_constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
+      | decode (Abs (x, T, t)) = Abs (x, T, decode t)
       | decode (t $ u) = decode t $ decode u
       | decode (Const (a, T)) =
           let val c =
             (case try Lexicon.unmark_const a of
               SOME c => c
             | NONE => snd (map_const a))
-          in Const (c, map_type T) end
+          in Const (c, T) end
       | decode (Free (a, T)) =
           (case (map_free a, map_const a) of
-            (SOME x, _) => Free (x, map_type T)
-          | (_, (true, c)) => Const (c, map_type T)
-          | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, map_type T))
-      | decode (Var (xi, T)) = Var (xi, map_type T)
+            (SOME x, _) => Free (x, T)
+          | (_, (true, c)) => Const (c, T)
+          | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, T))
+      | decode (Var (xi, T)) = Var (xi, T)
       | decode (t as Bound _) = t;
   in decode tm end;
 
@@ -144,10 +141,9 @@
 
 fun term_of_sort S =
   let
-    fun class c = Lexicon.const "_class" $ Lexicon.free c;
+    val class = Lexicon.const o Lexicon.mark_class;
 
-    fun classes [] = sys_error "term_of_sort"
-      | classes [c] = class c
+    fun classes [c] = class c
       | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
   in
     (case S of
@@ -165,7 +161,8 @@
       if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
       else t;
 
-    fun term_of (Type (a, Ts)) = Term.list_comb (Lexicon.const a, map term_of Ts)
+    fun term_of (Type (a, Ts)) =
+          Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
       | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
       | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   in term_of ty end;
@@ -193,15 +190,29 @@
 
 (* parse ast translations *)
 
-fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
-  | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
+val class_ast = Ast.Constant o Lexicon.mark_class;
+val type_ast = Ast.Constant o Lexicon.mark_type;
+
+fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c)
+  | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts);
+
+fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] =
+      Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast]
+  | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts);
 
-fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
-      Ast.Appl (f :: ty :: Ast.unfold_ast "_types" tys)
-  | tappl_ast_tr (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
+fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c)
+  | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts);
+
+fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] =
+      Ast.Appl [type_ast (read_type c), ty]
+  | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
+
+fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] =
+      Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys)
+  | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
 
 fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
-      Ast.fold_ast_p "fun" (Ast.unfold_ast "_types" dom, cod)
+      Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
   | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
 
 
@@ -212,10 +223,10 @@
   | tappl_ast_tr' (f, ty :: tys) =
       Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
 
-fun fun_ast_tr' (*"fun"*) asts =
+fun fun_ast_tr' (*"\\<^type>fun"*) asts =
   if no_brackets () orelse no_type_brackets () then raise Match
   else
-    (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
+    (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
       (dom as _ :: _ :: _, cod)
         => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
     | _ => raise Match);
@@ -229,20 +240,20 @@
 
 local open Lexicon SynExt in
 
-val type_ext = syn_ext' false (K false)
+fun type_ext {read_class, read_type} = syn_ext' false (K false)
   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
-   Mfix ("_",           idT --> typeT,                 "", [], max_pri),
-   Mfix ("_",           longidT --> typeT,             "", [], max_pri),
+   Mfix ("_",           idT --> typeT,                 "_type_name", [], max_pri),
+   Mfix ("_",           longidT --> typeT,             "_type_name", [], max_pri),
    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
    Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
-   Mfix ("_",           idT --> sortT,                 "", [], max_pri),
-   Mfix ("_",           longidT --> sortT,             "", [], max_pri),
+   Mfix ("_",           idT --> sortT,                 "_class_name", [], max_pri),
+   Mfix ("_",           longidT --> sortT,             "_class_name", [], max_pri),
    Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
    Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
-   Mfix ("_",           idT --> classesT,              "", [], max_pri),
-   Mfix ("_",           longidT --> classesT,          "", [], max_pri),
+   Mfix ("_",           idT --> classesT,              "_class_name", [], max_pri),
+   Mfix ("_",           longidT --> classesT,          "_class_name", [], max_pri),
    Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
    Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
@@ -251,16 +262,21 @@
    Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
-   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
+   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
-   Mfix ("'_",          typeT,                         "dummy", [], max_pri)]
+   Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
   []
   (map SynExt.mk_trfun
-   [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
+   [("_class_name", class_name_tr o read_class o ProofContext.theory_of),
+    ("_classes", classes_tr o read_class o ProofContext.theory_of),
+    ("_type_name", type_name_tr o read_type o ProofContext.theory_of),
+    ("_tapp", tapp_ast_tr o read_type o ProofContext.theory_of),
+    ("_tappl", tappl_ast_tr o read_type o ProofContext.theory_of),
+    ("_bracket", K bracket_ast_tr)],
    [],
    [],
-   map SynExt.mk_trfun [("fun", K fun_ast_tr')])
+   map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
   []
   ([], []);
 
diff -r bd7d6f65976e -r afa8cf9e63d8 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/pure_thy.ML	Wed Mar 03 00:28:22 2010 +0100
@@ -225,6 +225,8 @@
 
 val typ = Simple_Syntax.read_typ;
 val prop = Simple_Syntax.read_prop;
+
+val tycon = Syntax.mark_type;
 val const = Syntax.mark_const;
 
 val typeT = Syntax.typeT;
@@ -318,21 +320,21 @@
     (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
   #> Sign.add_syntax_i applC_syntax
   #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
-   [("fun",      typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
-    ("_bracket", typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
-    ("_ofsort",  typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
-    ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
-    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
-    ("_idtyp",    typ "id => type => idt",     Mixfix ("_\\<Colon>_", [], 0)),
-    ("_idtypdummy", typ "type => idt",         Mixfix ("'_()\\<Colon>_", [], 0)),
-    ("_type_constraint_", typ "'a",            NoSyn),
-    ("_lambda",  typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
-    (const "==", typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
-    (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
-    (const "==>", typ "prop => prop => prop",  Infixr ("\\<Longrightarrow>", 1)),
-    ("_DDDOT",   typ "aprop",                  Delimfix "\\<dots>"),
-    ("_bigimpl", typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
-    ("_DDDOT",   typ "logic",                  Delimfix "\\<dots>")]
+   [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
+    ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
+    ("_ofsort",           typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
+    ("_constrain",        typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
+    ("_constrain",        [spropT, typeT] ---> spropT,  Mixfix ("_\\<Colon>_", [4, 0], 3)),
+    ("_idtyp",            typ "id => type => idt",      Mixfix ("_\\<Colon>_", [], 0)),
+    ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
+    ("_type_constraint_", typ "'a",                     NoSyn),
+    ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
+    (const "==",          typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
+    (const "all_binder",  typ "idts => prop => prop",   Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
+    (const "==>",         typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
+    ("_DDDOT",            typ "aprop",                  Delimfix "\\<dots>"),
+    ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
+    ("_DDDOT",            typ "logic",                  Delimfix "\\<dots>")]
   #> Sign.add_modesyntax_i ("", false)
    [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
   #> Sign.add_modesyntax_i ("HTML", false)
diff -r bd7d6f65976e -r afa8cf9e63d8 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/sign.ML	Wed Mar 03 00:28:22 2010 +0100
@@ -56,10 +56,7 @@
   val intern_sort: theory -> sort -> sort
   val extern_sort: theory -> sort -> sort
   val intern_typ: theory -> typ -> typ
-  val extern_typ: theory -> typ -> typ
   val intern_term: theory -> term -> term
-  val extern_term: theory -> term -> term
-  val intern_tycons: theory -> typ -> typ
   val the_type_decl: theory -> string -> Type.decl
   val arity_number: theory -> string -> int
   val arity_sorts: theory -> string -> sort -> sort list
@@ -157,7 +154,7 @@
     make_sign (Name_Space.default_naming, syn, tsig, consts);
 
   val empty =
-    make_sign (Name_Space.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
+    make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
 
   fun merge pp (sign1, sign2) =
     let
@@ -266,41 +263,10 @@
   | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
   | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
 
-val add_classesT = Term.fold_atyps
-  (fn TFree (_, S) => fold (insert (op =)) S
-    | TVar (_, S) => fold (insert (op =)) S
-    | _ => I);
-
-fun add_tyconsT (Type (c, Ts)) = insert (op =) c #> fold add_tyconsT Ts
-  | add_tyconsT _ = I;
-
-val add_consts = Term.fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
-
-fun mapping add_names f t =
-  let
-    fun f' (x: string) = let val y = f x in if x = y then NONE else SOME (x, y) end;
-    val tab = map_filter f' (add_names t []);
-    fun get x = the_default x (AList.lookup (op =) tab x);
-  in get end;
-
-fun typ_mapping f g thy T =
-  T |> map_typ
-    (mapping add_classesT (f thy) T)
-    (mapping add_tyconsT (g thy) T);
-
-fun term_mapping f g h thy t =
-  t |> map_term
-    (mapping (Term.fold_types add_classesT) (f thy) t)
-    (mapping (Term.fold_types add_tyconsT) (g thy) t)
-    (mapping add_consts (h thy) t);
-
 in
 
-val intern_typ = typ_mapping intern_class intern_type;
-val extern_typ = typ_mapping extern_class extern_type;
-val intern_term = term_mapping intern_class intern_type intern_const;
-val extern_term = term_mapping extern_class extern_type (K Syntax.mark_const);
-val intern_tycons = typ_mapping (K I) intern_type;
+fun intern_typ thy = map_typ (intern_class thy) (intern_type thy);
+fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy);
 
 end;
 
@@ -424,6 +390,27 @@
 val cert_arity = prep_arity (K I) certify_sort;
 
 
+(* type syntax entities *)
+
+local
+
+fun read_type thy text =
+  let
+    val (syms, pos) = Syntax.read_token text;
+    val c = intern_type thy (Symbol_Pos.content syms);
+    val _ = the_type_decl thy c;
+    val _ = Position.report (Markup.tycon c) pos;
+  in c end;
+
+in
+
+val _ = Context.>>
+  (Context.map_theory
+    (map_syn (K (Syntax.basic_syntax {read_class = read_class, read_type = read_type}))));
+
+end;
+
+
 
 (** signature extension functions **)  (*exception ERROR/TYPE*)
 
@@ -438,11 +425,13 @@
 
 (* add type constructors *)
 
+val type_syntax = Syntax.mark_type oo full_name;
+
 fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
     val syn' =
       Syntax.update_type_gram true Syntax.mode_default
-        (map (fn (a, n, mx) => (Name.of_binding a, Syntax.make_type n, mx)) types) syn;
+        (map (fn (a, n, mx) => (type_syntax thy a, Syntax.make_type n, mx)) types) syn;
     val decls = map (fn (a, n, _) => (a, n)) types;
     val tsig' = fold (Type.add_type naming) decls tsig;
   in (naming, syn', tsig', consts) end);
@@ -452,9 +441,8 @@
 
 fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
-    val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
     val tsig' = fold (Type.add_nonterminal naming) ns tsig;
-  in (naming, syn', tsig', consts) end);
+  in (naming, syn, tsig', consts) end);
 
 
 (* add type abbreviations *)
@@ -465,7 +453,7 @@
       val ctxt = ProofContext.init thy;
       val syn' =
         Syntax.update_type_gram true Syntax.mode_default
-          [(Name.of_binding b, Syntax.make_type (length vs), mx)] syn;
+          [(type_syntax thy b, Syntax.make_type (length vs), mx)] syn;
       val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
         handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
       val tsig' = Type.add_abbrev naming abbr tsig;
@@ -495,8 +483,8 @@
 
 fun type_notation add mode args =
   let
-    fun type_syntax (Type (c, args), mx) =  (* FIXME authentic syntax *)
-          SOME (Long_Name.base_name c, Syntax.make_type (length args), mx)
+    fun type_syntax (Type (c, args), mx) =
+          SOME (Syntax.mark_type c, Syntax.make_type (length args), mx)
       | type_syntax _ = NONE;
   in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
 
@@ -579,9 +567,8 @@
 fun primitive_class (bclass, classes) thy =
   thy |> map_sign (fn (naming, syn, tsig, consts) =>
     let
-      val syn' = Syntax.update_consts [Name.of_binding bclass] syn;
       val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
-    in (naming, syn', tsig', consts) end)
+    in (naming, syn, tsig', consts) end)
   |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
 
 fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);