# HG changeset patch
# User haftmann
# Date 1268204690 -3600
# Node ID abf91fba0a70bbbb957f0ca484ccff92430547e8
# Parent  5e6811f4294b2ee290179faf0e77d98eab410e9c# Parent  2fa645db6e58446d2fd348c64e2055b7949b4c8b
merged

diff -r 2fa645db6e58 -r abf91fba0a70 NEWS
--- a/NEWS	Wed Mar 10 08:04:39 2010 +0100
+++ b/NEWS	Wed Mar 10 08:04:50 2010 +0100
@@ -76,6 +76,10 @@
 within a local theory context, with explicit checking of the
 constructors involved (in contrast to the raw 'syntax' versions).
 
+* Command 'typedecl' now works within a local theory context --
+without introducing dependencies on parameters or assumptions, which
+is not possible in Isabelle/Pure.
+
 
 *** HOL ***
 
diff -r 2fa645db6e58 -r abf91fba0a70 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Wed Mar 10 08:04:39 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Mar 10 08:04:50 2010 +0100
@@ -954,7 +954,7 @@
 text {*
   \begin{matharray}{rcll}
     @{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
   \end{matharray}
 
diff -r 2fa645db6e58 -r abf91fba0a70 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Mar 10 08:04:39 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Mar 10 08:04:50 2010 +0100
@@ -991,7 +991,7 @@
 \begin{isamarkuptext}%
 \begin{matharray}{rcll}
     \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
-    \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+    \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
   \end{matharray}
 
diff -r 2fa645db6e58 -r abf91fba0a70 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Wed Mar 10 08:04:50 2010 +0100
@@ -88,7 +88,7 @@
           let
             val args = Name.variant_list [] (replicate arity "'")
             val (T, thy') =
-              Typedecl.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
+              Typedecl.typedecl_global (Binding.name isa_name, args, mk_syntax name arity) thy
             val type_name = fst (Term.dest_Type T)
           in (((name, type_name), log_new name type_name), thy') end)
     end
diff -r 2fa645db6e58 -r abf91fba0a70 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 10 08:04:50 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 2fa645db6e58 -r abf91fba0a70 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Wed Mar 10 08:04:50 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 2fa645db6e58 -r abf91fba0a70 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/HOL/Tools/typedef.ML	Wed Mar 10 08:04:50 2010 +0100
@@ -130,7 +130,7 @@
           in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
 
     fun typedef_result inhabited =
-      Typedecl.typedecl (tname, vs, mx)
+      Typedecl.typedecl_global (tname, vs, mx)
       #> snd
       #> Sign.add_consts_i
         [(Rep_name, newT --> oldT, NoSyn),
diff -r 2fa645db6e58 -r abf91fba0a70 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/General/name_space.ML	Wed Mar 10 08:04:50 2010 +0100
@@ -47,6 +47,7 @@
   val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
   val declare: bool -> naming -> binding -> T -> string * T
+  val alias: naming -> binding -> string -> T -> T
   type 'a table = T * 'a Symtab.table
   val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
   val empty_table: string -> 'a table
@@ -72,8 +73,7 @@
 (* datatype entry *)
 
 type entry =
- {externals: xstring list,
-  concealed: bool,
+ {concealed: bool,
   group: serial option,
   theory_name: string,
   pos: Position.T,
@@ -96,7 +96,7 @@
   Name_Space of
    {kind: string,
     internals: (string list * string list) Symtab.table,  (*visible, hidden*)
-    entries: entry Symtab.table};
+    entries: (xstring list * entry) Symtab.table};        (*externals, entry*)
 
 fun make_name_space (kind, internals, entries) =
   Name_Space {kind = kind, internals = internals, entries = entries};
@@ -115,8 +115,7 @@
 fun the_entry (Name_Space {kind, entries, ...}) name =
   (case Symtab.lookup entries name of
     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
-  | SOME {concealed, group, theory_name, pos, id, ...} =>
-      {concealed = concealed, group = group, theory_name = theory_name, pos = pos, id = id});
+  | SOME (_, entry) => entry);
 
 fun is_concealed space name = #concealed (the_entry space name);
 
@@ -134,7 +133,7 @@
 fun get_accesses (Name_Space {entries, ...}) name =
   (case Symtab.lookup entries name of
     NONE => [name]
-  | SOME {externals, ...} => externals);
+  | SOME (externals, _) => externals);
 
 fun valid_accesses (Name_Space {internals, ...}) name =
   Symtab.fold (fn (xname, (names, _)) =>
@@ -212,7 +211,7 @@
         then raise Symtab.SAME
         else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
     val entries' = (entries1, entries2) |> Symtab.join
-      (fn name => fn (entry1, entry2) =>
+      (fn name => fn ((_, entry1), (_, entry2)) =>
         if #id entry1 = #id entry2 then raise Symtab.SAME
         else err_dup kind' (name, entry1) (name, entry2));
   in make_name_space (kind', internals', entries') end;
@@ -311,13 +310,13 @@
 
 (* declaration *)
 
-fun new_entry strict entry =
+fun new_entry strict (name, (externals, entry)) =
   map_name_space (fn (kind, internals, entries) =>
     let
       val entries' =
-        (if strict then Symtab.update_new else Symtab.update) entry entries
+        (if strict then Symtab.update_new else Symtab.update) (name, (externals, entry)) entries
           handle Symtab.DUP dup =>
-            err_dup kind (dup, the (Symtab.lookup entries dup)) entry;
+            err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
     in (kind, internals, entries') end);
 
 fun declare strict naming binding space =
@@ -330,16 +329,35 @@
     val _ = name = "" andalso err_bad binding;
 
     val entry =
-     {externals = accs',
-      concealed = concealed,
+     {concealed = concealed,
       group = group,
       theory_name = theory_name,
       pos = Position.default (Binding.pos_of binding),
       id = serial ()};
-    val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);
+    val space' = space
+      |> fold (add_name name) accs
+      |> new_entry strict (name, (accs', entry));
   in (name, space') end;
 
 
+(* alias *)
+
+fun alias naming binding name space =
+  let
+    val (accs, accs') = accesses naming binding;
+    val space' = space
+      |> fold (add_name name) accs
+      |> map_name_space (fn (kind, internals, entries) =>
+        let
+          val _ = Symtab.defined entries name orelse
+            error ("Undefined " ^ kind ^ " " ^ quote name);
+          val entries' = entries
+            |> Symtab.map_entry name (fn (externals, entry) =>
+              (Library.merge (op =) (externals, accs'), entry))
+        in (kind, internals, entries') end);
+  in space' end;
+
+
 
 (** name spaces coupled with symbol tables **)
 
diff -r 2fa645db6e58 -r abf91fba0a70 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Isar/class.ML	Wed Mar 10 08:04:50 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 2fa645db6e58 -r abf91fba0a70 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Isar/class_target.ML	Wed Mar 10 08:04:50 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 2fa645db6e58 -r abf91fba0a70 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 10 08:04:50 2010 +0100
@@ -103,16 +103,15 @@
 (* types *)
 
 val _ =
-  OuterSyntax.command "typedecl" "type declaration" K.thy_decl
-    (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
-      Toplevel.theory (Typedecl.typedecl (a, args, mx) #> snd)));
+  OuterSyntax.local_theory "typedecl" "type declaration" K.thy_decl
+    (P.type_args -- P.binding -- P.opt_mixfix
+      >> (fn ((args, a), mx) => Typedecl.typedecl (a, args, mx) #> snd));
 
 val _ =
   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
     (Scan.repeat1
       (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
-      >> (Toplevel.theory o Sign.add_tyabbrs o
-        map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
+      >> (Toplevel.theory o Sign.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
 
 val _ =
   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
diff -r 2fa645db6e58 -r abf91fba0a70 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 10 08:04:50 2010 +0100
@@ -27,6 +27,8 @@
   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 default_sort: Proof.context -> indexname -> sort
   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 +43,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 +58,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
@@ -122,6 +128,9 @@
     Context.generic -> Context.generic
   val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
+  val class_alias: binding -> class -> Proof.context -> Proof.context
+  val type_alias: binding -> string -> Proof.context -> Proof.context
+  val const_alias: binding -> string -> Proof.context -> Proof.context
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
@@ -167,16 +176,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 +195,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 +252,9 @@
 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;
+fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
+
 val consts_of = #1 o #consts o rep_context;
 val the_const_constraint = Consts.the_constraint o consts_of;
 
@@ -246,8 +264,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 +322,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 +473,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, default_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 +493,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 +525,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 +606,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 +624,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 +647,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 +731,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 +739,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 +749,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)
-      handle ERROR msg => cat_error msg  ("Failed to parse " ^ kind ^ Position.str_of 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
@@ -967,7 +1016,7 @@
 
 
 
-(** parameters **)
+(** basic logical entities **)
 
 (* variables *)
 
@@ -999,7 +1048,14 @@
 end;
 
 
-(* authentic constants *)
+(* authentic syntax *)
+
+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
 
@@ -1070,8 +1126,14 @@
       in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
   in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
 
+end;
 
-end;
+
+(* aliases *)
+
+fun class_alias b c ctxt = (map_tsigs o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
+fun type_alias b c ctxt = (map_tsigs o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
+fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
 
 
 (* local constants *)
diff -r 2fa645db6e58 -r abf91fba0a70 src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Isar/typedecl.ML	Wed Mar 10 08:04:50 2010 +0100
@@ -6,26 +6,50 @@
 
 signature TYPEDECL =
 sig
-  val typedecl: binding * string list * mixfix -> theory -> typ * theory
+  val typedecl: binding * string list * mixfix -> local_theory -> typ * local_theory
+  val typedecl_global: binding * string list * mixfix -> theory -> typ * theory
 end;
 
 structure Typedecl: TYPEDECL =
 struct
 
-fun typedecl (b, vs, mx) thy =
+fun typedecl (b, vs, mx) lthy =
   let
-    val base_sort = Object_Logic.get_base_sort thy;
-    val _ = has_duplicates (op =) vs andalso
-      error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
-    val name = Sign.full_name thy b;
+    fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
+    val _ = has_duplicates (op =) vs andalso err "Duplicate parameters";
+
+    val name = Local_Theory.full_name lthy b;
     val n = length vs;
-    val T = Type (name, map (fn v => TFree (v, [])) vs);
+    val args = map (fn a => TFree (a, ProofContext.default_sort lthy (a, ~1))) vs;
+    val T = Type (name, args);
+
+    val bad_args =
+      #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
+      |> filter_out Term.is_TVar;
+    val _ = not (null bad_args) andalso
+      err ("Locally fixed type arguments " ^ commas_quote (map (Syntax.string_of_typ lthy) bad_args));
+
+    val base_sort = Object_Logic.get_base_sort (ProofContext.theory_of lthy);
   in
-    thy
-    |> Sign.add_types [(b, n, mx)]
-    |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
+    lthy
+    |> Local_Theory.theory
+      (Sign.add_types [(b, n, NoSyn)] #>
+        (case base_sort of
+          NONE => I
+        | SOME S => AxClass.axiomatize_arity (name, replicate n S, S)))
+    |> Local_Theory.checkpoint
+    |> Local_Theory.type_notation true Syntax.mode_default [(T, mx)]
+    |> Local_Theory.type_syntax false
+      (fn _ => Context.mapping (Sign.type_alias b name) (ProofContext.type_alias b name))
+    |> ProofContext.type_alias b name
+    |> Variable.declare_typ T
     |> pair T
   end;
 
+fun typedecl_global decl =
+  Theory_Target.init NONE
+  #> typedecl decl
+  #> Local_Theory.exit_result_global Morphism.typ;
+
 end;
 
diff -r 2fa645db6e58 -r abf91fba0a70 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Mar 10 08:04:50 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 2fa645db6e58 -r abf91fba0a70 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/ROOT.ML	Wed Mar 10 08:04:50 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 2fa645db6e58 -r abf91fba0a70 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Mar 10 08:04:50 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 2fa645db6e58 -r abf91fba0a70 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Wed Mar 10 08:04:50 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 2fa645db6e58 -r abf91fba0a70 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/axclass.ML	Wed Mar 10 08:04:50 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 2fa645db6e58 -r abf91fba0a70 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/consts.ML	Wed Mar 10 08:04:50 2010 +0100
@@ -19,6 +19,7 @@
   val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   val the_constraint: T -> string -> typ                       (*exception TYPE*)
   val space_of: T -> Name_Space.T
+  val alias: Name_Space.naming -> binding -> string -> T -> T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
@@ -122,6 +123,9 @@
 
 fun space_of (Consts {decls = (space, _), ...}) = space;
 
+fun alias naming binding name = map_consts (fn ((space, decls), constraints, rev_abbrevs) =>
+  ((Name_Space.alias naming binding name space, decls), constraints, rev_abbrevs));
+
 val is_concealed = Name_Space.is_concealed o space_of;
 
 val intern = Name_Space.intern o space_of;
diff -r 2fa645db6e58 -r abf91fba0a70 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/sign.ML	Wed Mar 10 08:04:50 2010 +0100
@@ -47,17 +47,16 @@
   val class_space: theory -> Name_Space.T
   val type_space: theory -> Name_Space.T
   val const_space: theory -> Name_Space.T
+  val class_alias: binding -> class -> theory -> theory
+  val type_alias: binding -> string -> theory -> theory
+  val const_alias: binding -> string -> theory -> theory
   val intern_class: theory -> xstring -> string
   val extern_class: theory -> string -> xstring
   val intern_type: theory -> xstring -> string
   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 +70,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 +150,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,10 +232,14 @@
 
 (** 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;
 
+fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
+fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
+fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
+
 val intern_class = Name_Space.intern o class_space;
 val extern_class = Name_Space.extern o class_space;
 val intern_type = Name_Space.intern o type_space;
@@ -247,9 +247,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 +262,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 +272,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 +362,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 2fa645db6e58 -r abf91fba0a70 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Mar 10 08:04:39 2010 +0100
+++ b/src/Pure/type.ML	Wed Mar 10 08:04:50 2010 +0100
@@ -13,12 +13,17 @@
     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 class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
+  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 +40,11 @@
   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 type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
+  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 +113,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 +141,14 @@
 
 (* classes and sorts *)
 
+val class_space = #1 o #classes o rep_tsig;
+
+fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) =>
+  ((Name_Space.alias naming binding name space, classes), default, types));
+
+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 +183,18 @@
 fun restore_mode ctxt = set_mode (get_mode ctxt);
 
 
-(* lookup types *)
+(* types *)
+
+val type_space = #1 o #types o rep_tsig;
+
+fun type_alias naming binding name = map_tsig (fn (classes, default, (space, types)) =>
+  (classes, default, (Name_Space.alias naming binding name space, types)));
+
+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;