added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
added ProofContext.read_type_name_proper;
localized ProofContext.read_class/read_arity/cert_arity;
localized ProofContext.class_space/type_space etc.;

--- a/src/Pure/Isar/class.ML	Tue Mar 09 14:29:47 2010 +0100
+++ b/src/Pure/Isar/class.ML	Tue Mar 09 14:35:02 2010 +0100
@@ -338,7 +338,7 @@
 
 val subclass = gen_subclass (K I) user_proof;
 fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
-val subclass_cmd = gen_subclass Sign.read_class user_proof;
+val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init) user_proof;
 
 end; (*local*)
 

--- a/src/Pure/Isar/class_target.ML	Tue Mar 09 14:29:47 2010 +0100
+++ b/src/Pure/Isar/class_target.ML	Tue Mar 09 14:35:02 2010 +0100
@@ -417,7 +417,8 @@
 
 fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
   let
-    val all_arities = map (fn raw_tyco => Sign.read_arity thy
+    val ctxt = ProofContext.init thy;
+    val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
       (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
     val tycos = map #1 all_arities;
     val (_, sorts, sort) = hd all_arities;

--- a/src/Pure/Isar/proof_context.ML	Tue Mar 09 14:29:47 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 09 14:35:02 2010 +0100
@@ -27,6 +27,7 @@
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val full_name: Proof.context -> binding -> string
   val syn_of: Proof.context -> Syntax.syntax
+  val tsig_of: Proof.context -> Type.tsig
   val consts_of: Proof.context -> Consts.T
   val the_const_constraint: Proof.context -> string -> typ
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
@@ -41,6 +42,9 @@
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
+  val read_class: Proof.context -> xstring -> class
+  val read_arity: Proof.context -> xstring * string list * string -> arity
+  val cert_arity: Proof.context -> arity -> arity
   val read_typ: Proof.context -> string -> typ
   val read_typ_syntax: Proof.context -> string -> typ
   val read_typ_abbrev: Proof.context -> string -> typ
@@ -53,6 +57,7 @@
   val inferred_param: string -> Proof.context -> typ * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
   val read_type_name: Proof.context -> bool -> string -> typ
+  val read_type_name_proper: Proof.context -> bool -> string -> typ
   val read_const_proper: Proof.context -> bool -> string -> term
   val read_const: Proof.context -> bool -> string -> term
   val allow_dummies: Proof.context -> Proof.context
@@ -167,16 +172,17 @@
 
 datatype ctxt =
   Ctxt of
-   {mode: mode,                                       (*inner syntax mode*)
-    naming: Name_Space.naming,                        (*local naming conventions*)
-    syntax: Local_Syntax.T,                           (*local syntax*)
-    consts: Consts.T * Consts.T,                      (*local/global consts*)
-    facts: Facts.T,                                   (*local facts*)
+   {mode: mode,                       (*inner syntax mode*)
+    naming: Name_Space.naming,        (*local naming conventions*)
+    syntax: Local_Syntax.T,           (*local syntax*)
+    tsigs: Type.tsig * Type.tsig,     (*local/global type signature -- local name space only*)
+    consts: Consts.T * Consts.T,      (*local/global consts -- local name space/abbrevs only*)
+    facts: Facts.T,                   (*local facts*)
     cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
 
-fun make_ctxt (mode, naming, syntax, consts, facts, cases) =
+fun make_ctxt (mode, naming, syntax, tsigs, consts, facts, cases) =
   Ctxt {mode = mode, naming = naming, syntax = syntax,
-    consts = consts, facts = facts, cases = cases};
+    tsigs = tsigs, consts = consts, facts = facts, cases = cases};
 
 val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
 
@@ -185,41 +191,46 @@
   type T = ctxt;
   fun init thy =
     make_ctxt (mode_default, local_naming, Local_Syntax.init thy,
+      (Sign.tsig_of thy, Sign.tsig_of thy),
       (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
 );
 
 fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
 
 fun map_context f =
-  ContextData.map (fn Ctxt {mode, naming, syntax, consts, facts, cases} =>
-    make_ctxt (f (mode, naming, syntax, consts, facts, cases)));
+  ContextData.map (fn Ctxt {mode, naming, syntax, tsigs, consts, facts, cases} =>
+    make_ctxt (f (mode, naming, syntax, tsigs, consts, facts, cases)));
 
-fun set_mode mode = map_context (fn (_, naming, syntax, consts, facts, cases) =>
-  (mode, naming, syntax, consts, facts, cases));
+fun set_mode mode = map_context (fn (_, naming, syntax, tsigs, consts, facts, cases) =>
+  (mode, naming, syntax, tsigs, consts, facts, cases));
 
 fun map_mode f =
-  map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, consts, facts, cases) =>
-    (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, consts, facts, cases));
+  map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsigs, consts, facts, cases) =>
+    (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsigs, consts, facts, cases));
 
 fun map_naming f =
-  map_context (fn (mode, naming, syntax, consts, facts, cases) =>
-    (mode, f naming, syntax, consts, facts, cases));
+  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+    (mode, f naming, syntax, tsigs, consts, facts, cases));
 
 fun map_syntax f =
-  map_context (fn (mode, naming, syntax, consts, facts, cases) =>
-    (mode, naming, f syntax, consts, facts, cases));
+  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+    (mode, naming, f syntax, tsigs, consts, facts, cases));
+
+fun map_tsigs f =
+  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+    (mode, naming, syntax, f tsigs, consts, facts, cases));
 
 fun map_consts f =
-  map_context (fn (mode, naming, syntax, consts, facts, cases) =>
-    (mode, naming, syntax, f consts, facts, cases));
+  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+    (mode, naming, syntax, tsigs, f consts, facts, cases));
 
 fun map_facts f =
-  map_context (fn (mode, naming, syntax, consts, facts, cases) =>
-    (mode, naming, syntax, consts, f facts, cases));
+  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+    (mode, naming, syntax, tsigs, consts, f facts, cases));
 
 fun map_cases f =
-  map_context (fn (mode, naming, syntax, consts, facts, cases) =>
-    (mode, naming, syntax, consts, facts, f cases));
+  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
+    (mode, naming, syntax, tsigs, consts, facts, f cases));
 
 val get_mode = #mode o rep_context;
 val restore_mode = set_mode o get_mode;
@@ -237,6 +248,8 @@
 val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
 val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
 
+val tsig_of = #1 o #tsigs o rep_context;
+
 val consts_of = #1 o #consts o rep_context;
 val the_const_constraint = Consts.the_constraint o consts_of;
 
@@ -246,8 +259,13 @@
 
 (* theory transfer *)
 
-fun transfer_syntax thy =
-  map_syntax (Local_Syntax.rebuild thy) #>
+fun transfer_syntax thy ctxt = ctxt |>
+  map_syntax (Local_Syntax.rebuild thy) |>
+  map_tsigs (fn tsigs as (local_tsig, global_tsig) =>
+    let val thy_tsig = Sign.tsig_of thy in
+      if Type.eq_tsig (thy_tsig, global_tsig) then tsigs
+      else (Type.merge_tsigs (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig)
+    end) |>
   map_consts (fn consts as (local_consts, global_consts) =>
     let val thy_consts = Sign.consts_of thy in
       if Consts.eq_consts (thy_consts, global_consts) then consts
@@ -299,23 +317,49 @@
 
 (** prepare types **)
 
-(* read_typ *)
+(* classes *)
+
+fun read_class ctxt text =
+  let
+    val tsig = tsig_of ctxt;
+    val (syms, pos) = Syntax.read_token text;
+    val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
+      handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
+    val _ = Position.report (Markup.tclass c) pos;
+  in c end;
+
+
+(* type arities *)
+
+local
+
+fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
+  let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
+  in Type.add_arity (Syntax.pp ctxt) arity (tsig_of ctxt); arity end;
+
+in
+
+val read_arity = prep_arity (Type.intern_type o tsig_of) Syntax.read_sort;
+val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
+
+end;
+
+
+(* types *)
 
 fun read_typ_mode mode ctxt s =
   Syntax.read_typ (Type.set_mode mode ctxt) s;
 
-val read_typ        = read_typ_mode Type.mode_default;
+val read_typ = read_typ_mode Type.mode_default;
 val read_typ_syntax = read_typ_mode Type.mode_syntax;
 val read_typ_abbrev = read_typ_mode Type.mode_abbrev;
 
 
-(* cert_typ *)
-
 fun cert_typ_mode mode ctxt T =
-  Sign.certify_typ_mode mode (theory_of ctxt) T
+  Type.cert_typ_mode mode (tsig_of ctxt) T
     handle TYPE (msg, _, _) => error msg;
 
-val cert_typ        = cert_typ_mode Type.mode_default;
+val cert_typ = cert_typ_mode Type.mode_default;
 val cert_typ_syntax = cert_typ_mode Type.mode_syntax;
 val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev;
 
@@ -424,16 +468,16 @@
 
 fun read_type_name ctxt strict text =
   let
-    val thy = theory_of ctxt;
+    val tsig = tsig_of ctxt;
     val (c, pos) = token_content text;
   in
     if Syntax.is_tid c then
      (Position.report Markup.tfree pos;
-      TFree (c, the_default (Sign.defaultS thy) (Variable.def_sort ctxt (c, ~1))))
+      TFree (c, the_default (Type.defaultS tsig) (Variable.def_sort ctxt (c, ~1))))
     else
       let
-        val d = Sign.intern_type thy c;
-        val decl = Sign.the_type_decl thy d;
+        val d = Type.intern_type tsig c;
+        val decl = Type.the_decl tsig d;
         val _ = Position.report (Markup.tycon d) pos;
         fun err () = error ("Bad type name: " ^ quote d);
         val args =
@@ -444,6 +488,12 @@
       in Type (d, replicate args dummyT) end
   end;
 
+fun read_type_name_proper ctxt strict text =
+  (case read_type_name ctxt strict text of
+    T as Type _ => T
+  | T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
+
+
 fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
 
 fun read_const ctxt strict text =
@@ -470,8 +520,6 @@
 
 (* local abbreviations *)
 
-val tsig_of = Sign.tsig_of o ProofContext.theory_of;
-
 local
 
 fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
@@ -553,9 +601,9 @@
 
 (* types *)
 
-fun get_sort thy def_sort raw_env =
+fun get_sort ctxt def_sort raw_env =
   let
-    val tsig = Sign.tsig_of thy;
+    val tsig = tsig_of ctxt;
 
     fun eq ((xi, S), (xi', S')) =
       Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
@@ -571,8 +619,8 @@
       | (SOME S, NONE) => S
       | (SOME S, SOME S') =>
           if Type.eq_sort tsig (S, S') then S'
-          else error ("Sort constraint " ^ Syntax.string_of_sort_global thy S ^
-            " inconsistent with default " ^ Syntax.string_of_sort_global thy S' ^
+          else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
+            " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
             " for type variable " ^ quote (Term.string_of_vname' xi)));
   in get end;
 
@@ -594,12 +642,10 @@
 in
 
 fun term_context ctxt =
-  let val thy = theory_of ctxt in
-   {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)}
-  end;
+  {get_sort = get_sort ctxt (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)};
 
 fun decode_term ctxt =
   let val {get_sort, map_const, map_free} = term_context ctxt
@@ -680,8 +726,7 @@
 
 fun parse_typ ctxt text =
   let
-    val thy = theory_of ctxt;
-    val get_sort = get_sort thy (Variable.def_sort ctxt);
+    val get_sort = get_sort ctxt (Variable.def_sort ctxt);
     val (syms, pos) = Syntax.parse_token Markup.typ text;
     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);
@@ -689,7 +734,6 @@
 
 fun parse_term T ctxt text =
   let
-    val thy = theory_of ctxt;
     val {get_sort, map_const, map_free} = term_context ctxt;
 
     val (T', _) = TypeInfer.paramify_dummies T 0;
@@ -700,33 +744,33 @@
       handle ERROR msg => SOME msg;
     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)
+        ctxt (Type.is_logtype (tsig_of ctxt)) (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 =
-  Syntax.standard_unparse_sort {extern_class = Sign.extern_class (theory_of ctxt)}
+  Syntax.standard_unparse_sort {extern_class = Type.extern_class (tsig_of ctxt)}
     ctxt (syn_of ctxt);
 
 fun unparse_typ ctxt =
   let
-    val thy = theory_of ctxt;
-    val extern = {extern_class = Sign.extern_class thy, extern_type = Sign.extern_type thy};
+    val tsig = tsig_of ctxt;
+    val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
   in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end;
 
 fun unparse_term ctxt =
   let
-    val thy = theory_of ctxt;
+    val tsig = tsig_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_class = Type.extern_class tsig,
+      extern_type = Type.extern_type tsig,
       extern_const = Consts.extern consts};
   in
     Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
-      (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
+      (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax (theory_of ctxt)))
   end;
 
 in
@@ -999,7 +1043,14 @@
 end;
 
 
-(* authentic constants *)
+(* authentic logical entities *)
+
+val _ = Context.>>
+  (Context.map_theory
+    (Sign.add_advanced_trfuns
+      (Syntax.type_ast_trs
+        {read_class = read_class,
+          read_type = fn ctxt => #1 o dest_Type o read_type_name_proper ctxt false}, [], [], [])));
 
 local
 

--- a/src/Pure/ROOT.ML	Tue Mar 09 14:29:47 2010 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 09 14:35:02 2010 +0100
@@ -148,7 +148,6 @@
 use "assumption.ML";
 use "display.ML";
 use "goal.ML";
-use "axclass.ML";
 
 
 (* Isar -- Intelligible Semi-Automated Reasoning *)
@@ -209,6 +208,7 @@
 use "Isar/local_theory.ML";
 use "Isar/overloading.ML";
 use "Isar/locale.ML";
+use "axclass.ML";
 use "Isar/class_target.ML";
 use "Isar/theory_target.ML";
 use "Isar/expression.ML";

--- a/src/Pure/axclass.ML	Tue Mar 09 14:29:47 2010 +0100
+++ b/src/Pure/axclass.ML	Tue Mar 09 14:35:02 2010 +0100
@@ -280,7 +280,7 @@
   in (c1, c2) end;
 
 fun read_classrel thy raw_rel =
-  cert_classrel thy (pairself (Sign.read_class thy) raw_rel)
+  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
     handle TYPE (msg, _, _) => error msg;
 
 
@@ -387,7 +387,7 @@
 fun prove_arity raw_arity tac thy =
   let
     val ctxt = ProofContext.init thy;
-    val arity = Sign.cert_arity thy raw_arity;
+    val arity = ProofContext.cert_arity ctxt raw_arity;
     val names = map (prefix arity_prefix) (Logic.name_arities arity);
     val props = Logic.mk_arities arity;
     val ths = Goal.prove_multi ctxt [] [] props
@@ -530,7 +530,7 @@
     (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
 
 fun ax_arity prep =
-  axiomatize prep Logic.mk_arities
+  axiomatize (prep o ProofContext.init) Logic.mk_arities
     (map (prefix arity_prefix) o Logic.name_arities) add_arity;
 
 fun class_const c =
@@ -550,11 +550,11 @@
 in
 
 val axiomatize_class = ax_class Sign.certify_class cert_classrel;
-val axiomatize_class_cmd = ax_class Sign.read_class read_classrel;
+val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init) read_classrel;
 val axiomatize_classrel = ax_classrel cert_classrel;
 val axiomatize_classrel_cmd = ax_classrel read_classrel;
-val axiomatize_arity = ax_arity Sign.cert_arity;
-val axiomatize_arity_cmd = ax_arity Sign.read_arity;
+val axiomatize_arity = ax_arity ProofContext.cert_arity;
+val axiomatize_arity_cmd = ax_arity ProofContext.read_arity;
 
 end;
 

--- a/src/Pure/sign.ML	Tue Mar 09 14:29:47 2010 +0100
+++ b/src/Pure/sign.ML	Tue Mar 09 14:35:02 2010 +0100
@@ -53,11 +53,7 @@
   val extern_type: theory -> string -> xstring
   val intern_const: theory -> xstring -> string
   val extern_const: theory -> string -> xstring
-  val intern_sort: theory -> sort -> sort
-  val extern_sort: theory -> sort -> sort
-  val intern_typ: theory -> typ -> typ
   val intern_term: theory -> term -> term
-  val the_type_decl: theory -> string -> Type.decl
   val arity_number: theory -> string -> int
   val arity_sorts: theory -> string -> sort -> sort list
   val certify_class: theory -> class -> class
@@ -71,9 +67,6 @@
   val no_frees: Pretty.pp -> term -> term
   val no_vars: Pretty.pp -> term -> term
   val cert_def: Proof.context -> term -> (string * typ) * term
-  val read_class: theory -> xstring -> class
-  val read_arity: theory -> xstring * string list * string -> arity
-  val cert_arity: theory -> arity -> arity
   val add_defsort: string -> theory -> theory
   val add_defsort_i: sort -> theory -> theory
   val add_types: (binding * int * mixfix) list -> theory -> theory
@@ -154,7 +147,7 @@
     make_sign (Name_Space.default_naming, syn, tsig, consts);
 
   val empty =
-    make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
+    make_sign (Name_Space.default_naming, Syntax.basic_syntax, Type.empty_tsig, Consts.empty);
 
   fun merge pp (sign1, sign2) =
     let
@@ -236,8 +229,8 @@
 
 (** intern / extern names **)
 
-val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
-val type_space = #1 o #types o Type.rep_tsig o tsig_of;
+val class_space = Type.class_space o tsig_of;
+val type_space = Type.type_space o tsig_of;
 val const_space = Consts.space_of o consts_of;
 
 val intern_class = Name_Space.intern o class_space;
@@ -247,9 +240,6 @@
 val intern_const = Name_Space.intern o const_space;
 val extern_const = Name_Space.extern o const_space;
 
-val intern_sort = map o intern_class;
-val extern_sort = map o extern_class;
-
 local
 
 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
@@ -265,7 +255,6 @@
 
 in
 
-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;
@@ -276,7 +265,6 @@
 
 (* certify wrt. type signature *)
 
-val the_type_decl = Type.the_decl o tsig_of;
 val arity_number = Type.arity_number o tsig_of;
 fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
 
@@ -367,51 +355,6 @@
 
 
 
-(** read and certify entities **)    (*exception ERROR*)
-
-(* classes *)
-
-fun read_class thy text =
-  let
-    val (syms, pos) = Syntax.read_token text;
-    val c = certify_class thy (intern_class thy (Symbol_Pos.content syms))
-      handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
-    val _ = Position.report (Markup.tclass c) pos;
-  in c end;
-
-
-(* type arities *)
-
-fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =
-  let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
-  in Type.add_arity (Syntax.pp_global thy) arity (tsig_of thy); arity end;
-
-val read_arity = prep_arity intern_type Syntax.read_sort_global;
-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*)
 
 (* add default sort *)

--- a/src/Pure/type.ML	Tue Mar 09 14:29:47 2010 +0100
+++ b/src/Pure/type.ML	Tue Mar 09 14:35:02 2010 +0100
@@ -13,12 +13,16 @@
     Abbreviation of string list * typ * bool |
     Nonterminal
   type tsig
+  val eq_tsig: tsig * tsig -> bool
   val rep_tsig: tsig ->
    {classes: Name_Space.T * Sorts.algebra,
     default: sort,
     types: decl Name_Space.table,
     log_types: string list}
   val empty_tsig: tsig
+  val class_space: tsig -> Name_Space.T
+  val intern_class: tsig -> xstring -> string
+  val extern_class: tsig -> string -> xstring
   val defaultS: tsig -> sort
   val logical_types: tsig -> string list
   val eq_sort: tsig -> sort * sort -> bool
@@ -35,6 +39,10 @@
   val get_mode: Proof.context -> mode
   val set_mode: mode -> Proof.context -> Proof.context
   val restore_mode: Proof.context -> Proof.context -> Proof.context
+  val type_space: tsig -> Name_Space.T
+  val intern_type: tsig -> xstring -> string
+  val extern_type: tsig -> string -> xstring
+  val is_logtype: tsig -> string -> bool
   val the_decl: tsig -> string -> decl
   val cert_typ_mode: mode -> tsig -> typ -> typ
   val cert_typ: tsig -> typ -> typ
@@ -103,6 +111,13 @@
     types: decl Name_Space.table,           (*declared types*)
     log_types: string list};                (*logical types sorted by number of arguments*)
 
+fun eq_tsig
+   (TSig {classes = classes1, default = default1, types = types1, log_types = _},
+    TSig {classes = classes2, default = default2, types = types2, log_types = _}) =
+  pointer_eq (classes1, classes2) andalso
+  default1 = default2 andalso
+  pointer_eq (types1, types2);
+
 fun rep_tsig (TSig comps) = comps;
 
 fun make_tsig (classes, default, types, log_types) =
@@ -124,6 +139,11 @@
 
 (* classes and sorts *)
 
+val class_space = #1 o #classes o rep_tsig;
+
+val intern_class = Name_Space.intern o class_space;
+val extern_class = Name_Space.extern o class_space;
+
 fun defaultS (TSig {default, ...}) = default;
 fun logical_types (TSig {log_types, ...}) = log_types;
 
@@ -158,7 +178,15 @@
 fun restore_mode ctxt = set_mode (get_mode ctxt);
 
 
-(* lookup types *)
+(* types *)
+
+val type_space = #1 o #types o rep_tsig;
+
+val intern_type = Name_Space.intern o type_space;
+val extern_type = Name_Space.extern o type_space;
+
+val is_logtype = member (op =) o logical_types;
+
 
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;