# HG changeset patch
# User wenzelm
# Date 1268162599 -3600
# Node ID 86e48f81492b7ff906eaa5ddceb6360d625e8d3b
# Parent  b6720fe8afa795004e3b282b0e42dd7e40c7c4c6# Parent  3007b46c1660d754cb7e73ec3258bb40cbab912e
merged

diff -r b6720fe8afa7 -r 86e48f81492b src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Mar 09 20:23:19 2010 +0100
@@ -58,7 +58,7 @@
    val goal = List.nth(prems_of thm, i-1);
    val ps = Logic.strip_params goal;
    val Ts = rev (map snd ps);
-   fun is_of_fs_name T = Sign.of_sort thy (T, Sign.intern_sort thy ["fs_"^atom_basename]);
+   fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]);
 (* rebuild de bruijn indices *)
    val bvs = map_index (Bound o fst) ps;
 (* select variables of the right class *)
diff -r b6720fe8afa7 -r 86e48f81492b src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Tue Mar 09 20:23:19 2010 +0100
@@ -360,7 +360,7 @@
 
 
 (*For Isabelle, the lhs of a definition must be a constant.*)
-fun mk_const_def sign (c, Ty, rhs) =
+fun legacy_const_def sign (c, Ty, rhs) =
   singleton (Syntax.check_terms (ProofContext.init sign))
     (Sign.intern_term sign (Const("==",dummyT) $ Const(c,Ty) $ rhs));
 
@@ -385,7 +385,7 @@
      val wfrec_R_M =  map_types poly_tvars
                           (wfrec $ map_types poly_tvars R)
                       $ functional
-     val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
+     val def_term = legacy_const_def thy (x, Ty, wfrec_R_M)
      val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
  in (thy', def) end;
 end;
@@ -540,7 +540,7 @@
      val {lhs,rhs} = S.dest_eq proto_def'
      val (c,args) = S.strip_comb lhs
      val (name,Ty) = dest_atom c
-     val defn = mk_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
+     val defn = legacy_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
      val ([def0], theory) =
        thy
        |> PureThy.add_defs false
diff -r b6720fe8afa7 -r 86e48f81492b src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/Pure/Isar/class.ML	Tue Mar 09 20:23:19 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*)
 
diff -r b6720fe8afa7 -r 86e48f81492b src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/Pure/Isar/class_target.ML	Tue Mar 09 20:23:19 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;
diff -r b6720fe8afa7 -r 86e48f81492b src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 09 20:23:19 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
 
diff -r b6720fe8afa7 -r 86e48f81492b src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Tue Mar 09 20:23:19 2010 +0100
@@ -102,8 +102,8 @@
 
 (* type classes *)
 
-fun class syn = Args.theory -- Scan.lift Args.name_source >> (fn (thy, s) =>
-  Sign.read_class thy s
+fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
+  ProofContext.read_class ctxt s
   |> syn ? Syntax.mark_class
   |> ML_Syntax.print_string);
 
@@ -119,8 +119,8 @@
 fun type_name kind check = Args.context -- Scan.lift (OuterParse.position Args.name_source)
   >> (fn (ctxt, (s, pos)) =>
     let
-      val Type (c, _) = ProofContext.read_type_name ctxt false s;
-      val decl = Sign.the_type_decl (ProofContext.theory_of ctxt) c;
+      val Type (c, _) = ProofContext.read_type_name_proper ctxt false s;
+      val decl = Type.the_decl (ProofContext.tsig_of ctxt) c;
       val res =
         (case try check (c, decl) of
           SOME res => res
diff -r b6720fe8afa7 -r 86e48f81492b src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 09 20:23:19 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";
diff -r b6720fe8afa7 -r 86e48f81492b src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Mar 09 20:23:19 2010 +0100
@@ -29,10 +29,7 @@
   val mode_default: mode
   val mode_input: mode
   val merge_syntaxes: syntax -> syntax -> syntax
-  val empty_syntax: syntax
-  val basic_syntax:
-   {read_class: theory -> xstring -> string,
-    read_type: theory -> xstring -> string} -> syntax
+  val basic_syntax: syntax
   val basic_nonterms: string list
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
@@ -383,9 +380,9 @@
 
 (* basic syntax *)
 
-fun basic_syntax read =
+val basic_syntax =
   empty_syntax
-  |> update_syntax mode_default (TypeExt.type_ext read)
+  |> update_syntax mode_default TypeExt.type_ext
   |> update_syntax mode_default SynExt.pure_ext;
 
 val basic_nonterms =
diff -r b6720fe8afa7 -r 86e48f81492b src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Tue Mar 09 20:23:19 2010 +0100
@@ -15,6 +15,10 @@
   val term_of_typ: bool -> typ -> term
   val no_brackets: unit -> bool
   val no_type_brackets: unit -> bool
+  val type_ast_trs:
+   {read_class: Proof.context -> string -> string,
+    read_type: Proof.context -> string -> string} ->
+    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
 end;
 
 signature TYPE_EXT =
@@ -23,9 +27,7 @@
   val term_of_sort: sort -> term
   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val sortT: typ
-  val type_ext:
-   {read_class: theory -> string -> string,
-    read_type: theory -> string -> string} -> SynExt.syn_ext
+  val type_ext: SynExt.syn_ext
 end;
 
 structure TypeExt: TYPE_EXT =
@@ -240,7 +242,7 @@
 
 local open Lexicon SynExt in
 
-fun type_ext {read_class, read_type} = syn_ext' false (K false)
+val type_ext = syn_ext' false (K false)
   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
    Mfix ("_",           idT --> typeT,                 "_type_name", [], max_pri),
@@ -267,19 +269,18 @@
    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
    Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
   ["_type_prop"]
-  (map SynExt.mk_trfun
-   [("_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 [("\\<^type>fun", K fun_ast_tr')])
+  ([], [], [], map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
   []
   ([], []);
 
+fun type_ast_trs {read_class, read_type} =
+ [("_class_name", class_name_tr o read_class),
+  ("_classes", classes_tr o read_class),
+  ("_type_name", type_name_tr o read_type),
+  ("_tapp", tapp_ast_tr o read_type),
+  ("_tappl", tappl_ast_tr o read_type),
+  ("_bracket", K bracket_ast_tr)];
+
 end;
 
 end;
diff -r b6720fe8afa7 -r 86e48f81492b src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/Pure/axclass.ML	Tue Mar 09 20:23:19 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;
 
diff -r b6720fe8afa7 -r 86e48f81492b src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/Pure/sign.ML	Tue Mar 09 20:23:19 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 *)
diff -r b6720fe8afa7 -r 86e48f81492b src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/Pure/type.ML	Tue Mar 09 20:23:19 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;