authentic syntax for classes and type constructors;
authorwenzelm
Wed Mar 03 00:28:22 2010 +0100 (2010-03-03)
changeset 35429afa8cf9e63d8
parent 35428 bd7d6f65976e
child 35430 df2862dc23a8
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;
src/Pure/Isar/local_syntax.ML
src/Pure/Isar/proof_context.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/type_ext.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/local_syntax.ML	Wed Mar 03 00:00:44 2010 +0100
     1.2 +++ b/src/Pure/Isar/local_syntax.ML	Wed Mar 03 00:28:22 2010 +0100
     1.3 @@ -4,13 +4,11 @@
     1.4  Local syntax depending on theory syntax.
     1.5  *)
     1.6  
     1.7 -val show_structs = Unsynchronized.ref false;
     1.8 -
     1.9  signature LOCAL_SYNTAX =
    1.10  sig
    1.11    type T
    1.12    val syn_of: T -> Syntax.syntax
    1.13 -  val structs_of: T -> string list
    1.14 +  val idents_of: T -> {structs: string list, fixes: string list}
    1.15    val init: theory -> T
    1.16    val rebuild: theory -> T -> T
    1.17    datatype kind = Type | Const | Fixed
    1.18 @@ -19,7 +17,6 @@
    1.19    val restore_mode: T -> T -> T
    1.20    val update_modesyntax: theory -> bool -> Syntax.mode ->
    1.21      (kind * (string * typ * mixfix)) list -> T -> T
    1.22 -  val extern_term: T -> term -> term
    1.23  end;
    1.24  
    1.25  structure Local_Syntax: LOCAL_SYNTAX =
    1.26 @@ -49,8 +46,7 @@
    1.27    Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
    1.28  
    1.29  fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
    1.30 -fun idents_of (Syntax {idents, ...}) = idents;
    1.31 -val structs_of = #1 o idents_of;
    1.32 +fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
    1.33  
    1.34  
    1.35  (* build syntax *)
    1.36 @@ -125,21 +121,4 @@
    1.37  fun update_modesyntax thy add mode args syntax =
    1.38    syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
    1.39  
    1.40 -
    1.41 -(* extern_term *)
    1.42 -
    1.43 -fun extern_term syntax =
    1.44 -  let
    1.45 -    val (structs, fixes) = idents_of syntax;
    1.46 -    fun map_free (t as Free (x, T)) =
    1.47 -          let val i = find_index (fn s => s = x) structs + 1 in
    1.48 -            if i = 0 andalso member (op =) fixes x then
    1.49 -              Term.Const (Syntax.mark_fixed x, T)
    1.50 -            else if i = 1 andalso not (! show_structs) then
    1.51 -              Syntax.const "_struct" $ Syntax.const "_indexdefault"
    1.52 -            else t
    1.53 -          end
    1.54 -      | map_free t = t;
    1.55 -  in Term.map_aterms map_free end;
    1.56 -
    1.57  end;
     2.1 --- a/src/Pure/Isar/proof_context.ML	Wed Mar 03 00:00:44 2010 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 03 00:28:22 2010 +0100
     2.3 @@ -363,15 +363,11 @@
     2.4            (Pretty.str (setmp_CRITICAL show_question_marks true Term.string_of_vname (x', i))))
     2.5    | NONE => Pretty.mark Markup.var (Pretty.str s));
     2.6  
     2.7 -fun class_markup _ c =    (* FIXME authentic syntax *)
     2.8 -  Pretty.mark (Markup.tclassN, []) (Pretty.str c);
     2.9 -
    2.10  fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
    2.11  
    2.12  val token_trans =
    2.13   Syntax.tokentrans_mode ""
    2.14 -  [("class", class_markup),
    2.15 -   ("tfree", plain_markup Markup.tfree),
    2.16 +  [("tfree", plain_markup Markup.tfree),
    2.17     ("tvar", plain_markup Markup.tvar),
    2.18     ("free", free_or_skolem),
    2.19     ("bound", plain_markup Markup.bound),
    2.20 @@ -601,14 +597,12 @@
    2.21     {get_sort = get_sort thy (Variable.def_sort ctxt),
    2.22      map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
    2.23        handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
    2.24 -    map_free = intern_skolem ctxt (Variable.def_type ctxt false),
    2.25 -    map_type = Sign.intern_tycons thy,
    2.26 -    map_sort = Sign.intern_sort thy}
    2.27 +    map_free = intern_skolem ctxt (Variable.def_type ctxt false)}
    2.28    end;
    2.29  
    2.30  fun decode_term ctxt =
    2.31 -  let val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt
    2.32 -  in Syntax.decode_term get_sort map_const map_free map_type map_sort end;
    2.33 +  let val {get_sort, map_const, map_free} = term_context ctxt
    2.34 +  in Syntax.decode_term get_sort map_const map_free end;
    2.35  
    2.36  end;
    2.37  
    2.38 @@ -677,26 +671,23 @@
    2.39  fun parse_sort ctxt text =
    2.40    let
    2.41      val (syms, pos) = Syntax.parse_token Markup.sort text;
    2.42 -    val S = Syntax.standard_parse_sort ctxt (syn_of ctxt)
    2.43 -        (Sign.intern_sort (theory_of ctxt)) (syms, pos)
    2.44 +    val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
    2.45        handle ERROR msg => cat_error msg  ("Failed to parse sort" ^ Position.str_of pos)
    2.46    in S end;
    2.47  
    2.48  fun parse_typ ctxt text =
    2.49    let
    2.50 -    val thy = ProofContext.theory_of ctxt;
    2.51 +    val thy = theory_of ctxt;
    2.52      val get_sort = get_sort thy (Variable.def_sort ctxt);
    2.53 -
    2.54      val (syms, pos) = Syntax.parse_token Markup.typ text;
    2.55 -    val T = Sign.intern_tycons thy
    2.56 -        (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) (syms, pos))
    2.57 -      handle ERROR msg => cat_error msg  ("Failed to parse type" ^ Position.str_of pos);
    2.58 +    val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (syms, pos)
    2.59 +      handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
    2.60    in T end;
    2.61  
    2.62  fun parse_term T ctxt text =
    2.63    let
    2.64      val thy = theory_of ctxt;
    2.65 -    val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
    2.66 +    val {get_sort, map_const, map_free} = term_context ctxt;
    2.67  
    2.68      val (T', _) = TypeInfer.paramify_dummies T 0;
    2.69      val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
    2.70 @@ -704,29 +695,35 @@
    2.71  
    2.72      fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
    2.73        handle ERROR msg => SOME msg;
    2.74 -    val t = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
    2.75 -        map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
    2.76 +    val t =
    2.77 +      Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
    2.78 +        ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
    2.79        handle ERROR msg => cat_error msg  ("Failed to parse " ^ kind ^ Position.str_of pos);
    2.80    in t end;
    2.81  
    2.82  
    2.83 -fun unparse_sort ctxt S =
    2.84 -  Syntax.standard_unparse_sort ctxt (syn_of ctxt) (Sign.extern_sort (theory_of ctxt) S);
    2.85 +fun unparse_sort ctxt =
    2.86 +  Syntax.standard_unparse_sort {extern_class = Sign.extern_class (theory_of ctxt)}
    2.87 +    ctxt (syn_of ctxt);
    2.88  
    2.89 -fun unparse_typ ctxt T =
    2.90 -  Syntax.standard_unparse_typ ctxt (syn_of ctxt) (Sign.extern_typ (theory_of ctxt) T);
    2.91 +fun unparse_typ ctxt =
    2.92 +  let
    2.93 +    val thy = theory_of ctxt;
    2.94 +    val extern = {extern_class = Sign.extern_class thy, extern_type = Sign.extern_type thy};
    2.95 +  in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end;
    2.96  
    2.97 -fun unparse_term ctxt t =
    2.98 +fun unparse_term ctxt =
    2.99    let
   2.100      val thy = theory_of ctxt;
   2.101      val syntax = syntax_of ctxt;
   2.102      val consts = consts_of ctxt;
   2.103 +    val extern =
   2.104 +     {extern_class = Sign.extern_class thy,
   2.105 +      extern_type = Sign.extern_type thy,
   2.106 +      extern_const = Consts.extern consts};
   2.107    in
   2.108 -    t
   2.109 -    |> Sign.extern_term thy
   2.110 -    |> Local_Syntax.extern_term syntax
   2.111 -    |> Syntax.standard_unparse_term (Consts.extern consts) ctxt
   2.112 -        (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
   2.113 +    Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
   2.114 +      (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
   2.115    end;
   2.116  
   2.117  in
   2.118 @@ -1010,18 +1007,20 @@
   2.119        in Syntax.Constant d end
   2.120    | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
   2.121  
   2.122 +val typ = Simple_Syntax.read_typ;
   2.123 +
   2.124  in
   2.125  
   2.126  val _ = Context.>> (Context.map_theory
   2.127 - (Sign.add_syntax
   2.128 -   [("_context_const", "id => logic", Delimfix "CONST _"),
   2.129 -    ("_context_const", "id => aprop", Delimfix "CONST _"),
   2.130 -    ("_context_const", "longid => logic", Delimfix "CONST _"),
   2.131 -    ("_context_const", "longid => aprop", Delimfix "CONST _"),
   2.132 -    ("_context_xconst", "id => logic", Delimfix "XCONST _"),
   2.133 -    ("_context_xconst", "id => aprop", Delimfix "XCONST _"),
   2.134 -    ("_context_xconst", "longid => logic", Delimfix "XCONST _"),
   2.135 -    ("_context_xconst", "longid => aprop", Delimfix "XCONST _")] #>
   2.136 + (Sign.add_syntax_i
   2.137 +   [("_context_const", typ "id => logic", Delimfix "CONST _"),
   2.138 +    ("_context_const", typ "id => aprop", Delimfix "CONST _"),
   2.139 +    ("_context_const", typ "longid => logic", Delimfix "CONST _"),
   2.140 +    ("_context_const", typ "longid => aprop", Delimfix "CONST _"),
   2.141 +    ("_context_xconst", typ "id => logic", Delimfix "XCONST _"),
   2.142 +    ("_context_xconst", typ "id => aprop", Delimfix "XCONST _"),
   2.143 +    ("_context_xconst", typ "longid => logic", Delimfix "XCONST _"),
   2.144 +    ("_context_xconst", typ "longid => aprop", Delimfix "XCONST _")] #>
   2.145    Sign.add_advanced_trfuns
   2.146      ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
   2.147  
   2.148 @@ -1032,8 +1031,8 @@
   2.149  
   2.150  local
   2.151  
   2.152 -fun type_syntax (Type (c, args), mx) =  (* FIXME authentic syntax *)
   2.153 -      SOME (Local_Syntax.Type, (Long_Name.base_name c, Syntax.make_type (length args), mx))
   2.154 +fun type_syntax (Type (c, args), mx) =
   2.155 +      SOME (Local_Syntax.Type, (Syntax.mark_type c, Syntax.make_type (length args), mx))
   2.156    | type_syntax _ = NONE;
   2.157  
   2.158  fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
   2.159 @@ -1345,7 +1344,7 @@
   2.160        val prt_term = Syntax.pretty_term ctxt;
   2.161  
   2.162        (*structures*)
   2.163 -      val structs = Local_Syntax.structs_of (syntax_of ctxt);
   2.164 +      val {structs, ...} = Local_Syntax.idents_of (syntax_of ctxt);
   2.165        val prt_structs =
   2.166          if null structs then []
   2.167          else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
   2.168 @@ -1415,3 +1414,4 @@
   2.169    end;
   2.170  
   2.171  end;
   2.172 +
     3.1 --- a/src/Pure/ML/ml_antiquote.ML	Wed Mar 03 00:00:44 2010 +0100
     3.2 +++ b/src/Pure/ML/ml_antiquote.ML	Wed Mar 03 00:28:22 2010 +0100
     3.3 @@ -104,7 +104,7 @@
     3.4  
     3.5  fun class syn = Args.theory -- Scan.lift Args.name_source >> (fn (thy, s) =>
     3.6    Sign.read_class thy s
     3.7 -  |> syn ? Long_Name.base_name   (* FIXME authentic syntax *)
     3.8 +  |> syn ? Syntax.mark_class
     3.9    |> ML_Syntax.print_string);
    3.10  
    3.11  val _ = inline "class" (class false);
    3.12 @@ -130,7 +130,7 @@
    3.13  val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
    3.14  val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
    3.15  val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
    3.16 -val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Long_Name.base_name c));  (* FIXME authentic syntax *)
    3.17 +val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Syntax.mark_type c));
    3.18  
    3.19  
    3.20  (* constants *)
     4.1 --- a/src/Pure/Syntax/printer.ML	Wed Mar 03 00:00:44 2010 +0100
     4.2 +++ b/src/Pure/Syntax/printer.ML	Wed Mar 03 00:28:22 2010 +0100
     4.3 @@ -11,29 +11,32 @@
     4.4    val show_types: bool Unsynchronized.ref
     4.5    val show_no_free_types: bool Unsynchronized.ref
     4.6    val show_all_types: bool Unsynchronized.ref
     4.7 +  val show_structs: bool Unsynchronized.ref
     4.8    val pp_show_brackets: Pretty.pp -> Pretty.pp
     4.9  end;
    4.10  
    4.11  signature PRINTER =
    4.12  sig
    4.13    include PRINTER0
    4.14 -  val term_to_ast: Proof.context ->
    4.15 -    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
    4.16 +  val sort_to_ast: Proof.context ->
    4.17 +    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
    4.18    val typ_to_ast: Proof.context ->
    4.19      (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
    4.20 -  val sort_to_ast: Proof.context ->
    4.21 -    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
    4.22 +  val term_to_ast: {structs: string list, fixes: string list} -> string list -> Proof.context ->
    4.23 +    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
    4.24    type prtabs
    4.25    val empty_prtabs: prtabs
    4.26    val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
    4.27    val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
    4.28    val merge_prtabs: prtabs -> prtabs -> prtabs
    4.29 -  val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
    4.30 -    -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
    4.31 -    -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
    4.32 -  val pretty_typ_ast: Proof.context -> bool -> prtabs
    4.33 -    -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
    4.34 -    -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
    4.35 +  val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring,
    4.36 +      extern_const: string -> xstring} -> Proof.context -> bool -> prtabs ->
    4.37 +    (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
    4.38 +    (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
    4.39 +  val pretty_typ_ast: {extern_class: string -> xstring, extern_type: string -> xstring} ->
    4.40 +    Proof.context -> bool -> prtabs ->
    4.41 +    (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
    4.42 +    (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
    4.43  end;
    4.44  
    4.45  structure Printer: PRINTER =
    4.46 @@ -47,6 +50,7 @@
    4.47  val show_brackets = Unsynchronized.ref false;
    4.48  val show_no_free_types = Unsynchronized.ref false;
    4.49  val show_all_types = Unsynchronized.ref false;
    4.50 +val show_structs = Unsynchronized.ref false;
    4.51  
    4.52  fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
    4.53    Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
    4.54 @@ -84,8 +88,7 @@
    4.55  
    4.56  fun ast_of_termT ctxt trf tm =
    4.57    let
    4.58 -    fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
    4.59 -      | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
    4.60 +    fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
    4.61        | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
    4.62        | ast_of (Const (a, _)) = trans a []
    4.63        | ast_of (t as _ $ _) =
    4.64 @@ -105,19 +108,30 @@
    4.65  
    4.66  (** term_to_ast **)
    4.67  
    4.68 -fun mark_freevars ((t as Const (c, _)) $ u) =
    4.69 -      if member (op =) SynExt.standard_token_markers c then (t $ u)
    4.70 -      else t $ mark_freevars u
    4.71 -  | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
    4.72 -  | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
    4.73 -  | mark_freevars (t as Free _) = Lexicon.const "_free" $ t
    4.74 -  | mark_freevars (t as Var (xi, T)) =
    4.75 -      if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
    4.76 -      else Lexicon.const "_var" $ t
    4.77 -  | mark_freevars a = a;
    4.78 +fun ast_of_term idents consts ctxt trf
    4.79 +    show_all_types no_freeTs show_types show_sorts show_structs tm =
    4.80 +  let
    4.81 +    val {structs, fixes} = idents;
    4.82  
    4.83 -fun ast_of_term ctxt trf show_all_types no_freeTs show_types show_sorts tm =
    4.84 -  let
    4.85 +    fun mark_atoms ((t as Const (c, T)) $ u) =
    4.86 +          if member (op =) consts c then (t $ u)
    4.87 +          else Const (Lexicon.mark_const c, T) $ mark_atoms u
    4.88 +      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
    4.89 +      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
    4.90 +      | mark_atoms (Const (c, T)) = Const (Lexicon.mark_const c, T)
    4.91 +      | mark_atoms (t as Free (x, T)) =
    4.92 +          let val i = find_index (fn s => s = x) structs + 1 in
    4.93 +            if i = 0 andalso member (op =) fixes x then
    4.94 +              Term.Const (Lexicon.mark_fixed x, T)
    4.95 +            else if i = 1 andalso not show_structs then
    4.96 +              Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
    4.97 +            else Lexicon.const "_free" $ t
    4.98 +          end
    4.99 +      | mark_atoms (t as Var (xi, T)) =
   4.100 +          if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
   4.101 +          else Lexicon.const "_var" $ t
   4.102 +      | mark_atoms a = a;
   4.103 +
   4.104      fun prune_typs (t_seen as (Const _, _)) = t_seen
   4.105        | prune_typs (t as Free (x, ty), seen) =
   4.106            if ty = dummyT then (t, seen)
   4.107 @@ -148,9 +162,9 @@
   4.108            Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
   4.109        | (Const ("_idtdummy", T), ts) =>
   4.110            Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
   4.111 -      | (c' as Const (c, T), ts) =>
   4.112 +      | (const as Const (c, T), ts) =>
   4.113            if show_all_types
   4.114 -          then Ast.mk_appl (constrain c' T) (map ast_of ts)
   4.115 +          then Ast.mk_appl (constrain const T) (map ast_of ts)
   4.116            else trans c T ts
   4.117        | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
   4.118  
   4.119 @@ -162,18 +176,18 @@
   4.120        if show_types andalso T <> dummyT then
   4.121          Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
   4.122            ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
   4.123 -      else simple_ast_of t
   4.124 +      else simple_ast_of t;
   4.125    in
   4.126      tm
   4.127      |> SynTrans.prop_tr'
   4.128 -    |> (if show_types then #1 o prune_typs o rpair [] else I)
   4.129 -    |> mark_freevars
   4.130 +    |> show_types ? (#1 o prune_typs o rpair [])
   4.131 +    |> mark_atoms
   4.132      |> ast_of
   4.133    end;
   4.134  
   4.135 -fun term_to_ast ctxt trf tm =
   4.136 -  ast_of_term ctxt trf (! show_all_types) (! show_no_free_types)
   4.137 -    (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
   4.138 +fun term_to_ast idents consts ctxt trf tm =
   4.139 +  ast_of_term idents consts ctxt trf (! show_all_types) (! show_no_free_types)
   4.140 +    (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;
   4.141  
   4.142  
   4.143  
   4.144 @@ -267,8 +281,10 @@
   4.145    | is_chain [Arg _] = true
   4.146    | is_chain _  = false;
   4.147  
   4.148 -fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
   4.149 +fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 p0 =
   4.150    let
   4.151 +    val {extern_class, extern_type, extern_const} = extern;
   4.152 +
   4.153      fun token_trans a x =
   4.154        (case tokentrf a of
   4.155          NONE =>
   4.156 @@ -291,7 +307,7 @@
   4.157              val (Ts, args') = synT markup (symbs, args);
   4.158            in
   4.159              if type_mode then (astT (t, p) @ Ts, args')
   4.160 -            else (pretty I ctxt tabs trf tokentrf true curried t p @ Ts, args')
   4.161 +            else (pretty extern ctxt tabs trf tokentrf true curried t p @ Ts, args')
   4.162            end
   4.163        | synT markup (String s :: symbs, args) =
   4.164            let val (Ts, args') = synT markup (symbs, args);
   4.165 @@ -312,7 +328,6 @@
   4.166              val (Ts, args') = synT markup (symbs, args);
   4.167              val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
   4.168            in (T :: Ts, args') end
   4.169 -      | synT _ (_ :: _, []) = sys_error "synT"
   4.170  
   4.171      and parT markup (pr, args, p, p': int) = #1 (synT markup
   4.172            (if p > p' orelse
   4.173 @@ -320,13 +335,12 @@
   4.174              then [Block (1, Space "(" :: pr @ [Space ")"])]
   4.175              else pr, args))
   4.176  
   4.177 -    and atomT a =
   4.178 -      (case try Lexicon.unmark_const a of
   4.179 -        SOME c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c))
   4.180 -      | NONE =>
   4.181 -          (case try Lexicon.unmark_fixed a of
   4.182 -            SOME x => the (token_trans "_free" x)
   4.183 -          | NONE => Pretty.str a))
   4.184 +    and atomT a = a |> Lexicon.unmark
   4.185 +     {case_class = fn c => Pretty.mark (Markup.tclass c) (Pretty.str (extern_class c)),
   4.186 +      case_type = fn c => Pretty.mark (Markup.tycon c) (Pretty.str (extern_type c)),
   4.187 +      case_const = fn c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c)),
   4.188 +      case_fixed = fn x => the (token_trans "_free" x),
   4.189 +      case_default = Pretty.str}
   4.190  
   4.191      and prefixT (_, a, [], _) = [atomT a]
   4.192        | prefixT (c, _, args, p) = astT (appT (c, args), p)
   4.193 @@ -334,15 +348,16 @@
   4.194      and splitT 0 ([x], ys) = (x, ys)
   4.195        | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
   4.196        | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
   4.197 -      | splitT _ _ = sys_error "splitT"
   4.198  
   4.199      and combT (tup as (c, a, args, p)) =
   4.200        let
   4.201          val nargs = length args;
   4.202 -        val markup = Pretty.mark
   4.203 -          (Markup.const (Lexicon.unmark_const a) handle Fail _ =>
   4.204 -            (Markup.fixed (Lexicon.unmark_fixed a)))
   4.205 -          handle Fail _ => I;
   4.206 +        val markup = a |> Lexicon.unmark
   4.207 +         {case_class = Pretty.mark o Markup.tclass,
   4.208 +          case_type = Pretty.mark o Markup.tycon,
   4.209 +          case_const = Pretty.mark o Markup.const,
   4.210 +          case_fixed = Pretty.mark o Markup.fixed,
   4.211 +          case_default = K I};
   4.212  
   4.213          (*find matching table entry, or print as prefix / postfix*)
   4.214          fun prnt ([], []) = prefixT tup
   4.215 @@ -371,15 +386,16 @@
   4.216  
   4.217  (* pretty_term_ast *)
   4.218  
   4.219 -fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
   4.220 -  pretty extern_const ctxt (mode_tabs prtabs (print_mode_value ()))
   4.221 +fun pretty_term_ast extern ctxt curried prtabs trf tokentrf ast =
   4.222 +  pretty extern ctxt (mode_tabs prtabs (print_mode_value ()))
   4.223      trf tokentrf false curried ast 0;
   4.224  
   4.225  
   4.226  (* pretty_typ_ast *)
   4.227  
   4.228 -fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
   4.229 -  pretty I ctxt (mode_tabs prtabs (print_mode_value ()))
   4.230 +fun pretty_typ_ast {extern_class, extern_type} ctxt _ prtabs trf tokentrf ast =
   4.231 +  pretty {extern_class = extern_class, extern_type = extern_type, extern_const = I}
   4.232 +    ctxt (mode_tabs prtabs (print_mode_value ()))
   4.233      trf tokentrf true false ast 0;
   4.234  
   4.235  end;
     5.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Mar 03 00:00:44 2010 +0100
     5.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Mar 03 00:28:22 2010 +0100
     5.3 @@ -282,7 +282,8 @@
     5.4        if not (exists is_index args) then (const, typ, [])
     5.5        else
     5.6          let
     5.7 -          val indexed_const = if const <> "" then "_indexed_" ^ const
     5.8 +          val indexed_const =
     5.9 +            if const <> "" then const ^ "_indexed"
    5.10              else err_in_mfix "Missing constant name for indexed syntax" mfix;
    5.11            val rangeT = Term.range_type typ handle Match =>
    5.12              err_in_mfix "Missing structure argument for indexed syntax" mfix;
    5.13 @@ -387,7 +388,7 @@
    5.14  fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
    5.15  
    5.16  val standard_token_classes =
    5.17 -  ["class", "tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
    5.18 +  ["tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
    5.19  
    5.20  val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
    5.21  
     6.1 --- a/src/Pure/Syntax/syn_trans.ML	Wed Mar 03 00:00:44 2010 +0100
     6.2 +++ b/src/Pure/Syntax/syn_trans.ML	Wed Mar 03 00:28:22 2010 +0100
     6.3 @@ -34,16 +34,16 @@
     6.4    val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
     6.5    val constrainAbsC: string
     6.6    val pure_trfuns:
     6.7 -      (string * (Ast.ast list -> Ast.ast)) list *
     6.8 -      (string * (term list -> term)) list *
     6.9 -      (string * (term list -> term)) list *
    6.10 -      (string * (Ast.ast list -> Ast.ast)) list
    6.11 +    (string * (Ast.ast list -> Ast.ast)) list *
    6.12 +    (string * (term list -> term)) list *
    6.13 +    (string * (term list -> term)) list *
    6.14 +    (string * (Ast.ast list -> Ast.ast)) list
    6.15    val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
    6.16    val struct_trfuns: string list ->
    6.17 -      (string * (Ast.ast list -> Ast.ast)) list *
    6.18 -      (string * (term list -> term)) list *
    6.19 -      (string * (bool -> typ -> term list -> term)) list *
    6.20 -      (string * (Ast.ast list -> Ast.ast)) list
    6.21 +    (string * (Ast.ast list -> Ast.ast)) list *
    6.22 +    (string * (term list -> term)) list *
    6.23 +    (string * (bool -> typ -> term list -> term)) list *
    6.24 +    (string * (Ast.ast list -> Ast.ast)) list
    6.25  end;
    6.26  
    6.27  signature SYN_TRANS =
    6.28 @@ -131,7 +131,7 @@
    6.29  
    6.30  fun mk_type ty =
    6.31    Lexicon.const "_constrain" $
    6.32 -    Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "itself" $ ty);
    6.33 +    Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
    6.34  
    6.35  fun ofclass_tr (*"_ofclass"*) [ty, cls] = cls $ mk_type ty
    6.36    | ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts);
    6.37 @@ -143,7 +143,7 @@
    6.38  
    6.39  (* meta propositions *)
    6.40  
    6.41 -fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "prop"
    6.42 +fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
    6.43    | aprop_tr (*"_aprop"*) ts = raise TERM ("aprop_tr", ts);
    6.44  
    6.45  
    6.46 @@ -195,7 +195,8 @@
    6.47  fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
    6.48    | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
    6.49    | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
    6.50 -      list_comb (c $ update_name_tr [t] $ (Lexicon.const "fun" $ ty $ Lexicon.const "dummy"), ts)
    6.51 +      list_comb (c $ update_name_tr [t] $
    6.52 +        (Lexicon.const "\\<^type>fun" $ ty $ Lexicon.const "\\<^type>dummy"), ts)
    6.53    | update_name_tr ts = raise TERM ("update_name_tr", ts);
    6.54  
    6.55  
    6.56 @@ -368,7 +369,7 @@
    6.57      fun is_prop Ts t =
    6.58        fastype_of1 (Ts, t) = propT handle TERM _ => false;
    6.59  
    6.60 -    fun is_term (Const ("\\<^const>Pure.term", _) $ _) = true
    6.61 +    fun is_term (Const ("Pure.term", _) $ _) = true
    6.62        | is_term _ = false;
    6.63  
    6.64      fun tr' _ (t as Const _) = t
    6.65 @@ -381,7 +382,7 @@
    6.66        | tr' Ts (t as Bound _) =
    6.67            if is_prop Ts t then aprop t else t
    6.68        | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
    6.69 -      | tr' Ts (t as t1 $ (t2 as Const ("\\<^const>TYPE", Type ("itself", [T])))) =
    6.70 +      | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
    6.71            if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
    6.72            else tr' Ts t1 $ tr' Ts t2
    6.73        | tr' Ts (t as t1 $ t2) =
    6.74 @@ -568,7 +569,7 @@
    6.75  
    6.76      val free_fixed = Term.map_aterms
    6.77        (fn t as Const (c, T) =>
    6.78 -          (case try (unprefix Lexicon.fixedN) c of
    6.79 +          (case try Lexicon.unmark_fixed c of
    6.80              NONE => t
    6.81            | SOME x => Free (x, T))
    6.82          | t => t);
     7.1 --- a/src/Pure/Syntax/syntax.ML	Wed Mar 03 00:00:44 2010 +0100
     7.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Mar 03 00:28:22 2010 +0100
     7.3 @@ -29,7 +29,10 @@
     7.4    val mode_default: mode
     7.5    val mode_input: mode
     7.6    val merge_syntaxes: syntax -> syntax -> syntax
     7.7 -  val basic_syn: syntax
     7.8 +  val empty_syntax: syntax
     7.9 +  val basic_syntax:
    7.10 +   {read_class: theory -> xstring -> string,
    7.11 +    read_type: theory -> xstring -> string} -> syntax
    7.12    val basic_nonterms: string list
    7.13    val print_gram: syntax -> unit
    7.14    val print_trans: syntax -> unit
    7.15 @@ -41,25 +44,24 @@
    7.16    val ambiguity_limit: int Unsynchronized.ref
    7.17    val standard_parse_term: Pretty.pp -> (term -> string option) ->
    7.18      (((string * int) * sort) list -> string * int -> Term.sort) ->
    7.19 -    (string -> bool * string) -> (string -> string option) ->
    7.20 -    (typ -> typ) -> (sort -> sort) -> Proof.context ->
    7.21 +    (string -> bool * string) -> (string -> string option) -> Proof.context ->
    7.22      (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
    7.23    val standard_parse_typ: Proof.context -> syntax ->
    7.24 -    ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
    7.25 -    Symbol_Pos.T list * Position.T -> typ
    7.26 -  val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) ->
    7.27 -    Symbol_Pos.T list * Position.T -> sort
    7.28 +    ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
    7.29 +  val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
    7.30    datatype 'a trrule =
    7.31      ParseRule of 'a * 'a |
    7.32      PrintRule of 'a * 'a |
    7.33      ParsePrintRule of 'a * 'a
    7.34    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
    7.35    val is_const: syntax -> string -> bool
    7.36 -  val standard_unparse_term: (string -> xstring) ->
    7.37 -    Proof.context -> syntax -> bool -> term -> Pretty.T
    7.38 -  val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
    7.39 -  val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
    7.40 -  val update_consts: string list -> syntax -> syntax
    7.41 +  val standard_unparse_term: {structs: string list, fixes: string list} ->
    7.42 +    {extern_class: string -> xstring, extern_type: string -> xstring,
    7.43 +      extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
    7.44 +  val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
    7.45 +    Proof.context -> syntax -> typ -> Pretty.T
    7.46 +  val standard_unparse_sort: {extern_class: string -> xstring} ->
    7.47 +    Proof.context -> syntax -> sort -> Pretty.T
    7.48    val update_trfuns:
    7.49      (string * ((ast list -> ast) * stamp)) list *
    7.50      (string * ((term list -> term) * stamp)) list *
    7.51 @@ -300,7 +302,7 @@
    7.52        lexicon =
    7.53          if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
    7.54        gram = if changed then Parser.extend_gram gram xprods else gram,
    7.55 -      consts = Library.merge (op =) (consts1, filter_out (can Lexicon.unmark_const) consts2),
    7.56 +      consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
    7.57        prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
    7.58        parse_ast_trtab =
    7.59          update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
    7.60 @@ -381,9 +383,9 @@
    7.61  
    7.62  (* basic syntax *)
    7.63  
    7.64 -val basic_syn =
    7.65 +fun basic_syntax read =
    7.66    empty_syntax
    7.67 -  |> update_syntax mode_default TypeExt.type_ext
    7.68 +  |> update_syntax mode_default (TypeExt.type_ext read)
    7.69    |> update_syntax mode_default SynExt.pure_ext;
    7.70  
    7.71  val basic_nonterms =
    7.72 @@ -547,26 +549,25 @@
    7.73              map (Pretty.string_of_term pp) (take limit results)))
    7.74        end;
    7.75  
    7.76 -fun standard_parse_term pp check get_sort map_const map_free map_type map_sort
    7.77 -    ctxt is_logtype syn ty (syms, pos) =
    7.78 +fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
    7.79    read ctxt is_logtype syn ty (syms, pos)
    7.80 -  |> map (TypeExt.decode_term get_sort map_const map_free map_type map_sort)
    7.81 +  |> map (TypeExt.decode_term get_sort map_const map_free)
    7.82    |> disambig (Printer.pp_show_brackets pp) check;
    7.83  
    7.84  
    7.85  (* read types *)
    7.86  
    7.87 -fun standard_parse_typ ctxt syn get_sort map_sort (syms, pos) =
    7.88 +fun standard_parse_typ ctxt syn get_sort (syms, pos) =
    7.89    (case read ctxt (K false) syn SynExt.typeT (syms, pos) of
    7.90 -    [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts map_sort t)) map_sort t
    7.91 +    [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts t)) t
    7.92    | _ => error (ambiguity_msg pos));
    7.93  
    7.94  
    7.95  (* read sorts *)
    7.96  
    7.97 -fun standard_parse_sort ctxt syn map_sort (syms, pos) =
    7.98 +fun standard_parse_sort ctxt syn (syms, pos) =
    7.99    (case read ctxt (K false) syn TypeExt.sortT (syms, pos) of
   7.100 -    [t] => TypeExt.sort_of_term map_sort t
   7.101 +    [t] => TypeExt.sort_of_term t
   7.102    | _ => error (ambiguity_msg pos));
   7.103  
   7.104  
   7.105 @@ -640,8 +641,8 @@
   7.106  
   7.107  fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
   7.108    let
   7.109 -    val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
   7.110 -    val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
   7.111 +    val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
   7.112 +    val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
   7.113    in
   7.114      Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
   7.115        (lookup_tokentr tokentrtab (print_mode_value ()))
   7.116 @@ -650,14 +651,16 @@
   7.117  
   7.118  in
   7.119  
   7.120 -fun standard_unparse_term extern =
   7.121 -  unparse_t Printer.term_to_ast (Printer.pretty_term_ast extern) Markup.term;
   7.122 +fun standard_unparse_term idents extern =
   7.123 +  unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
   7.124  
   7.125 -fun standard_unparse_typ ctxt syn =
   7.126 -  unparse_t Printer.typ_to_ast Printer.pretty_typ_ast Markup.typ ctxt syn false;
   7.127 +fun standard_unparse_typ extern ctxt syn =
   7.128 +  unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
   7.129  
   7.130 -fun standard_unparse_sort ctxt syn =
   7.131 -  unparse_t Printer.sort_to_ast Printer.pretty_typ_ast Markup.sort ctxt syn false;
   7.132 +fun standard_unparse_sort {extern_class} ctxt syn =
   7.133 +  unparse_t (K Printer.sort_to_ast)
   7.134 +    (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
   7.135 +    Markup.sort ctxt syn false;
   7.136  
   7.137  end;
   7.138  
   7.139 @@ -667,7 +670,6 @@
   7.140  
   7.141  fun ext_syntax f decls = update_syntax mode_default (f decls);
   7.142  
   7.143 -val update_consts = ext_syntax SynExt.syn_ext_const_names;
   7.144  val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
   7.145  val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
   7.146  val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
     8.1 --- a/src/Pure/Syntax/type_ext.ML	Wed Mar 03 00:00:44 2010 +0100
     8.2 +++ b/src/Pure/Syntax/type_ext.ML	Wed Mar 03 00:28:22 2010 +0100
     8.3 @@ -1,19 +1,17 @@
     8.4  (*  Title:      Pure/Syntax/type_ext.ML
     8.5      Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     8.6  
     8.7 -Utilities for input and output of types.  Also the concrete syntax of
     8.8 -types, which is required to bootstrap Pure.
     8.9 +Utilities for input and output of types.  The concrete syntax of types.
    8.10  *)
    8.11  
    8.12  signature TYPE_EXT0 =
    8.13  sig
    8.14 -  val sort_of_term: (sort -> sort) -> term -> sort
    8.15 -  val term_sorts: (sort -> sort) -> term -> (indexname * sort) list
    8.16 -  val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
    8.17 +  val sort_of_term: term -> sort
    8.18 +  val term_sorts: term -> (indexname * sort) list
    8.19 +  val typ_of_term: (indexname -> sort) -> term -> typ
    8.20    val type_constraint: typ -> term -> term
    8.21    val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
    8.22 -    (string -> bool * string) -> (string -> string option) ->
    8.23 -    (typ -> typ) -> (sort -> sort) -> term -> term
    8.24 +    (string -> bool * string) -> (string -> string option) -> term -> term
    8.25    val term_of_typ: bool -> typ -> term
    8.26    val no_brackets: unit -> bool
    8.27    val no_type_brackets: unit -> bool
    8.28 @@ -25,7 +23,9 @@
    8.29    val term_of_sort: sort -> term
    8.30    val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    8.31    val sortT: typ
    8.32 -  val type_ext: SynExt.syn_ext
    8.33 +  val type_ext:
    8.34 +   {read_class: theory -> string -> string,
    8.35 +    read_type: theory -> string -> string} -> SynExt.syn_ext
    8.36  end;
    8.37  
    8.38  structure TypeExt: TYPE_EXT =
    8.39 @@ -35,30 +35,28 @@
    8.40  
    8.41  (* sort_of_term *)
    8.42  
    8.43 -fun sort_of_term (map_sort: sort -> sort) tm =
    8.44 +fun sort_of_term tm =
    8.45    let
    8.46 -    fun classes (Const (c, _)) = [c]
    8.47 -      | classes (Free (c, _)) = [c]
    8.48 -      | classes (Const ("_class", _) $ Free (c, _)) = [c]
    8.49 -      | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
    8.50 -      | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
    8.51 -      | classes (Const ("_classes", _) $ (Const ("_class", _) $ Free (c, _)) $ cs) = c :: classes cs
    8.52 -      | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
    8.53 +    fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
    8.54 +
    8.55 +    fun class s = Lexicon.unmark_class s handle Fail _ => err ();
    8.56 +
    8.57 +    fun classes (Const (s, _)) = [class s]
    8.58 +      | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
    8.59 +      | classes _ = err ();
    8.60  
    8.61      fun sort (Const ("_topsort", _)) = []
    8.62 -      | sort (Const (c, _)) = [c]
    8.63 -      | sort (Free (c, _)) = [c]
    8.64 -      | sort (Const ("_class", _) $ Free (c, _)) = [c]
    8.65 +      | sort (Const (s, _)) = [class s]
    8.66        | sort (Const ("_sort", _) $ cs) = classes cs
    8.67 -      | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
    8.68 -  in map_sort (sort tm) end;
    8.69 +      | sort _ = err ();
    8.70 +  in sort tm end;
    8.71  
    8.72  
    8.73  (* term_sorts *)
    8.74  
    8.75 -fun term_sorts map_sort tm =
    8.76 +fun term_sorts tm =
    8.77    let
    8.78 -    val sort_of = sort_of_term map_sort;
    8.79 +    val sort_of = sort_of_term;
    8.80  
    8.81      fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
    8.82            insert (op =) ((x, ~1), sort_of cs)
    8.83 @@ -76,11 +74,11 @@
    8.84  
    8.85  (* typ_of_term *)
    8.86  
    8.87 -fun typ_of_term get_sort map_sort t =
    8.88 +fun typ_of_term get_sort tm =
    8.89    let
    8.90 -    fun typ_of (Free (x, _)) =
    8.91 -          if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
    8.92 -          else Type (x, [])
    8.93 +    fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
    8.94 +
    8.95 +    fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
    8.96        | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
    8.97        | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
    8.98        | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
    8.99 @@ -90,17 +88,16 @@
   8.100        | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
   8.101        | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
   8.102            TVar (xi, get_sort xi)
   8.103 -      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term map_sort t)
   8.104 -      | typ_of tm =
   8.105 +      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
   8.106 +      | typ_of t =
   8.107            let
   8.108 -            val (t, ts) = Term.strip_comb tm;
   8.109 +            val (head, args) = Term.strip_comb t;
   8.110              val a =
   8.111 -              (case t of
   8.112 -                Const (x, _) => x
   8.113 -              | Free (x, _) => x
   8.114 -              | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
   8.115 -          in Type (a, map typ_of ts) end;
   8.116 -  in typ_of t end;
   8.117 +              (case head of
   8.118 +                Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
   8.119 +              | _ => err ());
   8.120 +          in Type (a, map typ_of args) end;
   8.121 +  in typ_of tm end;
   8.122  
   8.123  
   8.124  (* decode_term -- transform parse tree into raw term *)
   8.125 @@ -109,30 +106,30 @@
   8.126    if T = dummyT then t
   8.127    else Const ("_type_constraint_", T --> T) $ t;
   8.128  
   8.129 -fun decode_term get_sort map_const map_free map_type map_sort tm =
   8.130 +fun decode_term get_sort map_const map_free tm =
   8.131    let
   8.132 -    val sort_env = term_sorts map_sort tm;
   8.133 -    val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort;
   8.134 +    val sort_env = term_sorts tm;
   8.135 +    val decodeT = typ_of_term (get_sort sort_env);
   8.136  
   8.137      fun decode (Const ("_constrain", _) $ t $ typ) =
   8.138            type_constraint (decodeT typ) (decode t)
   8.139        | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
   8.140            if T = dummyT then Abs (x, decodeT typ, decode t)
   8.141 -          else type_constraint (decodeT typ --> dummyT) (Abs (x, map_type T, decode t))
   8.142 -      | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t)
   8.143 +          else type_constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
   8.144 +      | decode (Abs (x, T, t)) = Abs (x, T, decode t)
   8.145        | decode (t $ u) = decode t $ decode u
   8.146        | decode (Const (a, T)) =
   8.147            let val c =
   8.148              (case try Lexicon.unmark_const a of
   8.149                SOME c => c
   8.150              | NONE => snd (map_const a))
   8.151 -          in Const (c, map_type T) end
   8.152 +          in Const (c, T) end
   8.153        | decode (Free (a, T)) =
   8.154            (case (map_free a, map_const a) of
   8.155 -            (SOME x, _) => Free (x, map_type T)
   8.156 -          | (_, (true, c)) => Const (c, map_type T)
   8.157 -          | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, map_type T))
   8.158 -      | decode (Var (xi, T)) = Var (xi, map_type T)
   8.159 +            (SOME x, _) => Free (x, T)
   8.160 +          | (_, (true, c)) => Const (c, T)
   8.161 +          | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, T))
   8.162 +      | decode (Var (xi, T)) = Var (xi, T)
   8.163        | decode (t as Bound _) = t;
   8.164    in decode tm end;
   8.165  
   8.166 @@ -144,10 +141,9 @@
   8.167  
   8.168  fun term_of_sort S =
   8.169    let
   8.170 -    fun class c = Lexicon.const "_class" $ Lexicon.free c;
   8.171 +    val class = Lexicon.const o Lexicon.mark_class;
   8.172  
   8.173 -    fun classes [] = sys_error "term_of_sort"
   8.174 -      | classes [c] = class c
   8.175 +    fun classes [c] = class c
   8.176        | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
   8.177    in
   8.178      (case S of
   8.179 @@ -165,7 +161,8 @@
   8.180        if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
   8.181        else t;
   8.182  
   8.183 -    fun term_of (Type (a, Ts)) = Term.list_comb (Lexicon.const a, map term_of Ts)
   8.184 +    fun term_of (Type (a, Ts)) =
   8.185 +          Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
   8.186        | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
   8.187        | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   8.188    in term_of ty end;
   8.189 @@ -193,15 +190,29 @@
   8.190  
   8.191  (* parse ast translations *)
   8.192  
   8.193 -fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
   8.194 -  | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
   8.195 +val class_ast = Ast.Constant o Lexicon.mark_class;
   8.196 +val type_ast = Ast.Constant o Lexicon.mark_type;
   8.197 +
   8.198 +fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c)
   8.199 +  | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts);
   8.200 +
   8.201 +fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] =
   8.202 +      Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast]
   8.203 +  | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts);
   8.204  
   8.205 -fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
   8.206 -      Ast.Appl (f :: ty :: Ast.unfold_ast "_types" tys)
   8.207 -  | tappl_ast_tr (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
   8.208 +fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c)
   8.209 +  | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts);
   8.210 +
   8.211 +fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] =
   8.212 +      Ast.Appl [type_ast (read_type c), ty]
   8.213 +  | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
   8.214 +
   8.215 +fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] =
   8.216 +      Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys)
   8.217 +  | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
   8.218  
   8.219  fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
   8.220 -      Ast.fold_ast_p "fun" (Ast.unfold_ast "_types" dom, cod)
   8.221 +      Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
   8.222    | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
   8.223  
   8.224  
   8.225 @@ -212,10 +223,10 @@
   8.226    | tappl_ast_tr' (f, ty :: tys) =
   8.227        Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
   8.228  
   8.229 -fun fun_ast_tr' (*"fun"*) asts =
   8.230 +fun fun_ast_tr' (*"\\<^type>fun"*) asts =
   8.231    if no_brackets () orelse no_type_brackets () then raise Match
   8.232    else
   8.233 -    (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
   8.234 +    (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
   8.235        (dom as _ :: _ :: _, cod)
   8.236          => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
   8.237      | _ => raise Match);
   8.238 @@ -229,20 +240,20 @@
   8.239  
   8.240  local open Lexicon SynExt in
   8.241  
   8.242 -val type_ext = syn_ext' false (K false)
   8.243 +fun type_ext {read_class, read_type} = syn_ext' false (K false)
   8.244    [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   8.245     Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
   8.246 -   Mfix ("_",           idT --> typeT,                 "", [], max_pri),
   8.247 -   Mfix ("_",           longidT --> typeT,             "", [], max_pri),
   8.248 +   Mfix ("_",           idT --> typeT,                 "_type_name", [], max_pri),
   8.249 +   Mfix ("_",           longidT --> typeT,             "_type_name", [], max_pri),
   8.250     Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
   8.251     Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
   8.252     Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
   8.253 -   Mfix ("_",           idT --> sortT,                 "", [], max_pri),
   8.254 -   Mfix ("_",           longidT --> sortT,             "", [], max_pri),
   8.255 +   Mfix ("_",           idT --> sortT,                 "_class_name", [], max_pri),
   8.256 +   Mfix ("_",           longidT --> sortT,             "_class_name", [], max_pri),
   8.257     Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
   8.258     Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
   8.259 -   Mfix ("_",           idT --> classesT,              "", [], max_pri),
   8.260 -   Mfix ("_",           longidT --> classesT,          "", [], max_pri),
   8.261 +   Mfix ("_",           idT --> classesT,              "_class_name", [], max_pri),
   8.262 +   Mfix ("_",           longidT --> classesT,          "_class_name", [], max_pri),
   8.263     Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
   8.264     Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
   8.265     Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
   8.266 @@ -251,16 +262,21 @@
   8.267     Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
   8.268     Mfix ("_",           typeT --> typesT,              "", [], max_pri),
   8.269     Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
   8.270 -   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
   8.271 +   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
   8.272     Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
   8.273     Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
   8.274 -   Mfix ("'_",          typeT,                         "dummy", [], max_pri)]
   8.275 +   Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
   8.276    []
   8.277    (map SynExt.mk_trfun
   8.278 -   [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
   8.279 +   [("_class_name", class_name_tr o read_class o ProofContext.theory_of),
   8.280 +    ("_classes", classes_tr o read_class o ProofContext.theory_of),
   8.281 +    ("_type_name", type_name_tr o read_type o ProofContext.theory_of),
   8.282 +    ("_tapp", tapp_ast_tr o read_type o ProofContext.theory_of),
   8.283 +    ("_tappl", tappl_ast_tr o read_type o ProofContext.theory_of),
   8.284 +    ("_bracket", K bracket_ast_tr)],
   8.285     [],
   8.286     [],
   8.287 -   map SynExt.mk_trfun [("fun", K fun_ast_tr')])
   8.288 +   map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
   8.289    []
   8.290    ([], []);
   8.291  
     9.1 --- a/src/Pure/pure_thy.ML	Wed Mar 03 00:00:44 2010 +0100
     9.2 +++ b/src/Pure/pure_thy.ML	Wed Mar 03 00:28:22 2010 +0100
     9.3 @@ -225,6 +225,8 @@
     9.4  
     9.5  val typ = Simple_Syntax.read_typ;
     9.6  val prop = Simple_Syntax.read_prop;
     9.7 +
     9.8 +val tycon = Syntax.mark_type;
     9.9  val const = Syntax.mark_const;
    9.10  
    9.11  val typeT = Syntax.typeT;
    9.12 @@ -318,21 +320,21 @@
    9.13      (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
    9.14    #> Sign.add_syntax_i applC_syntax
    9.15    #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
    9.16 -   [("fun",      typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
    9.17 -    ("_bracket", typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
    9.18 -    ("_ofsort",  typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
    9.19 -    ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    9.20 -    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
    9.21 -    ("_idtyp",    typ "id => type => idt",     Mixfix ("_\\<Colon>_", [], 0)),
    9.22 -    ("_idtypdummy", typ "type => idt",         Mixfix ("'_()\\<Colon>_", [], 0)),
    9.23 -    ("_type_constraint_", typ "'a",            NoSyn),
    9.24 -    ("_lambda",  typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    9.25 -    (const "==", typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
    9.26 -    (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
    9.27 -    (const "==>", typ "prop => prop => prop",  Infixr ("\\<Longrightarrow>", 1)),
    9.28 -    ("_DDDOT",   typ "aprop",                  Delimfix "\\<dots>"),
    9.29 -    ("_bigimpl", typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
    9.30 -    ("_DDDOT",   typ "logic",                  Delimfix "\\<dots>")]
    9.31 +   [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
    9.32 +    ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
    9.33 +    ("_ofsort",           typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
    9.34 +    ("_constrain",        typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    9.35 +    ("_constrain",        [spropT, typeT] ---> spropT,  Mixfix ("_\\<Colon>_", [4, 0], 3)),
    9.36 +    ("_idtyp",            typ "id => type => idt",      Mixfix ("_\\<Colon>_", [], 0)),
    9.37 +    ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
    9.38 +    ("_type_constraint_", typ "'a",                     NoSyn),
    9.39 +    ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    9.40 +    (const "==",          typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
    9.41 +    (const "all_binder",  typ "idts => prop => prop",   Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
    9.42 +    (const "==>",         typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
    9.43 +    ("_DDDOT",            typ "aprop",                  Delimfix "\\<dots>"),
    9.44 +    ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
    9.45 +    ("_DDDOT",            typ "logic",                  Delimfix "\\<dots>")]
    9.46    #> Sign.add_modesyntax_i ("", false)
    9.47     [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
    9.48    #> Sign.add_modesyntax_i ("HTML", false)
    10.1 --- a/src/Pure/sign.ML	Wed Mar 03 00:00:44 2010 +0100
    10.2 +++ b/src/Pure/sign.ML	Wed Mar 03 00:28:22 2010 +0100
    10.3 @@ -56,10 +56,7 @@
    10.4    val intern_sort: theory -> sort -> sort
    10.5    val extern_sort: theory -> sort -> sort
    10.6    val intern_typ: theory -> typ -> typ
    10.7 -  val extern_typ: theory -> typ -> typ
    10.8    val intern_term: theory -> term -> term
    10.9 -  val extern_term: theory -> term -> term
   10.10 -  val intern_tycons: theory -> typ -> typ
   10.11    val the_type_decl: theory -> string -> Type.decl
   10.12    val arity_number: theory -> string -> int
   10.13    val arity_sorts: theory -> string -> sort -> sort list
   10.14 @@ -157,7 +154,7 @@
   10.15      make_sign (Name_Space.default_naming, syn, tsig, consts);
   10.16  
   10.17    val empty =
   10.18 -    make_sign (Name_Space.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
   10.19 +    make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
   10.20  
   10.21    fun merge pp (sign1, sign2) =
   10.22      let
   10.23 @@ -266,41 +263,10 @@
   10.24    | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
   10.25    | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
   10.26  
   10.27 -val add_classesT = Term.fold_atyps
   10.28 -  (fn TFree (_, S) => fold (insert (op =)) S
   10.29 -    | TVar (_, S) => fold (insert (op =)) S
   10.30 -    | _ => I);
   10.31 -
   10.32 -fun add_tyconsT (Type (c, Ts)) = insert (op =) c #> fold add_tyconsT Ts
   10.33 -  | add_tyconsT _ = I;
   10.34 -
   10.35 -val add_consts = Term.fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
   10.36 -
   10.37 -fun mapping add_names f t =
   10.38 -  let
   10.39 -    fun f' (x: string) = let val y = f x in if x = y then NONE else SOME (x, y) end;
   10.40 -    val tab = map_filter f' (add_names t []);
   10.41 -    fun get x = the_default x (AList.lookup (op =) tab x);
   10.42 -  in get end;
   10.43 -
   10.44 -fun typ_mapping f g thy T =
   10.45 -  T |> map_typ
   10.46 -    (mapping add_classesT (f thy) T)
   10.47 -    (mapping add_tyconsT (g thy) T);
   10.48 -
   10.49 -fun term_mapping f g h thy t =
   10.50 -  t |> map_term
   10.51 -    (mapping (Term.fold_types add_classesT) (f thy) t)
   10.52 -    (mapping (Term.fold_types add_tyconsT) (g thy) t)
   10.53 -    (mapping add_consts (h thy) t);
   10.54 -
   10.55  in
   10.56  
   10.57 -val intern_typ = typ_mapping intern_class intern_type;
   10.58 -val extern_typ = typ_mapping extern_class extern_type;
   10.59 -val intern_term = term_mapping intern_class intern_type intern_const;
   10.60 -val extern_term = term_mapping extern_class extern_type (K Syntax.mark_const);
   10.61 -val intern_tycons = typ_mapping (K I) intern_type;
   10.62 +fun intern_typ thy = map_typ (intern_class thy) (intern_type thy);
   10.63 +fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy);
   10.64  
   10.65  end;
   10.66  
   10.67 @@ -424,6 +390,27 @@
   10.68  val cert_arity = prep_arity (K I) certify_sort;
   10.69  
   10.70  
   10.71 +(* type syntax entities *)
   10.72 +
   10.73 +local
   10.74 +
   10.75 +fun read_type thy text =
   10.76 +  let
   10.77 +    val (syms, pos) = Syntax.read_token text;
   10.78 +    val c = intern_type thy (Symbol_Pos.content syms);
   10.79 +    val _ = the_type_decl thy c;
   10.80 +    val _ = Position.report (Markup.tycon c) pos;
   10.81 +  in c end;
   10.82 +
   10.83 +in
   10.84 +
   10.85 +val _ = Context.>>
   10.86 +  (Context.map_theory
   10.87 +    (map_syn (K (Syntax.basic_syntax {read_class = read_class, read_type = read_type}))));
   10.88 +
   10.89 +end;
   10.90 +
   10.91 +
   10.92  
   10.93  (** signature extension functions **)  (*exception ERROR/TYPE*)
   10.94  
   10.95 @@ -438,11 +425,13 @@
   10.96  
   10.97  (* add type constructors *)
   10.98  
   10.99 +val type_syntax = Syntax.mark_type oo full_name;
  10.100 +
  10.101  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
  10.102    let
  10.103      val syn' =
  10.104        Syntax.update_type_gram true Syntax.mode_default
  10.105 -        (map (fn (a, n, mx) => (Name.of_binding a, Syntax.make_type n, mx)) types) syn;
  10.106 +        (map (fn (a, n, mx) => (type_syntax thy a, Syntax.make_type n, mx)) types) syn;
  10.107      val decls = map (fn (a, n, _) => (a, n)) types;
  10.108      val tsig' = fold (Type.add_type naming) decls tsig;
  10.109    in (naming, syn', tsig', consts) end);
  10.110 @@ -452,9 +441,8 @@
  10.111  
  10.112  fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
  10.113    let
  10.114 -    val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
  10.115      val tsig' = fold (Type.add_nonterminal naming) ns tsig;
  10.116 -  in (naming, syn', tsig', consts) end);
  10.117 +  in (naming, syn, tsig', consts) end);
  10.118  
  10.119  
  10.120  (* add type abbreviations *)
  10.121 @@ -465,7 +453,7 @@
  10.122        val ctxt = ProofContext.init thy;
  10.123        val syn' =
  10.124          Syntax.update_type_gram true Syntax.mode_default
  10.125 -          [(Name.of_binding b, Syntax.make_type (length vs), mx)] syn;
  10.126 +          [(type_syntax thy b, Syntax.make_type (length vs), mx)] syn;
  10.127        val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
  10.128          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
  10.129        val tsig' = Type.add_abbrev naming abbr tsig;
  10.130 @@ -495,8 +483,8 @@
  10.131  
  10.132  fun type_notation add mode args =
  10.133    let
  10.134 -    fun type_syntax (Type (c, args), mx) =  (* FIXME authentic syntax *)
  10.135 -          SOME (Long_Name.base_name c, Syntax.make_type (length args), mx)
  10.136 +    fun type_syntax (Type (c, args), mx) =
  10.137 +          SOME (Syntax.mark_type c, Syntax.make_type (length args), mx)
  10.138        | type_syntax _ = NONE;
  10.139    in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
  10.140  
  10.141 @@ -579,9 +567,8 @@
  10.142  fun primitive_class (bclass, classes) thy =
  10.143    thy |> map_sign (fn (naming, syn, tsig, consts) =>
  10.144      let
  10.145 -      val syn' = Syntax.update_consts [Name.of_binding bclass] syn;
  10.146        val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
  10.147 -    in (naming, syn', tsig', consts) end)
  10.148 +    in (naming, syn, tsig', consts) end)
  10.149    |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
  10.150  
  10.151  fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);