# HG changeset patch
# User wenzelm
# Date 1272230800 -7200
# Node ID c827275e530ec49efceda313240e4318a91b1c29
# Parent  2623a1987e1d92deafeb5c3c11f60696a03d6734# Parent  0584e203960e36d9658fea6d37cd5342fd816921
merged

diff -r 2623a1987e1d -r c827275e530e src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -99,7 +99,7 @@
     |> (fn ctxt1 => ctxt1
     |> prepare
     |-> (fn us => fn ctxt2 => ctxt2
-    |> Proof.theorem_i NONE (fn thmss => fn ctxt =>
+    |> Proof.theorem NONE (fn thmss => fn ctxt =>
          let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
          in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
   end
@@ -188,7 +188,7 @@
 
   fun prove thy meth vc =
     ProofContext.init thy
-    |> Proof.theorem_i NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
+    |> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
     |> Proof.apply meth
     |> Seq.hd
     |> Proof.global_done_proof
diff -r 2623a1987e1d -r c827275e530e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/HOL.thy	Sun Apr 25 23:26:40 2010 +0200
@@ -1869,7 +1869,7 @@
 proof
   assume "PROP ?ofclass"
   show "PROP ?eq"
-    by (tactic {* ALLGOALS (rtac (Drule.unconstrainTs @{thm equals_eq})) *}) 
+    by (tactic {* ALLGOALS (rtac (Thm.unconstrain_allTs @{thm equals_eq})) *}) 
       (fact `PROP ?ofclass`)
 next
   assume "PROP ?eq"
diff -r 2623a1987e1d -r c827275e530e src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -543,7 +543,7 @@
 
   in
     ctxt'' |>
-    Proof.theorem_i NONE (fn thss => fn ctxt =>
+    Proof.theorem NONE (fn thss => fn ctxt =>
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
diff -r 2623a1987e1d -r c827275e530e src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -445,7 +445,7 @@
 
   in
     ctxt'' |>
-    Proof.theorem_i NONE (fn thss => fn ctxt =>
+    Proof.theorem NONE (fn thss => fn ctxt =>
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
diff -r 2623a1987e1d -r c827275e530e src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -363,7 +363,7 @@
   in
     lthy' |>
     Variable.add_fixes (map fst lsrs) |> snd |>
-    Proof.theorem_i NONE
+    Proof.theorem NONE
       (fn thss => fn goal_ctxt =>
          let
            val simps = ProofContext.export goal_ctxt lthy' (flat thss);
diff -r 2623a1987e1d -r c827275e530e src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -436,7 +436,7 @@
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
+    |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
   end;
 
 val rep_datatype = gen_rep_datatype Sign.cert_term;
diff -r 2623a1987e1d -r c827275e530e src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/Function/function.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -120,7 +120,7 @@
       end
   in
     lthy
-    |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
+    |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
     |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
   end
 
@@ -177,7 +177,7 @@
     |> ProofContext.note_thmss ""
        [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
          [([Goal.norm_result termination], [])])] |> snd
-    |> Proof.theorem_i NONE afterqed [[(goal, [])]]
+    |> Proof.theorem NONE afterqed [[(goal, [])]]
   end
 
 val termination_proof = gen_termination_proof Syntax.check_term
diff -r 2623a1987e1d -r c827275e530e src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -3059,7 +3059,7 @@
            ) options [const]))
       end
   in
-    Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
+    Proof.theorem NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
   end;
 
 val code_pred = generic_code_pred (K I);
diff -r 2623a1987e1d -r c827275e530e src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -45,7 +45,7 @@
   val goals' = map (rpair []) goals
   fun after_qed' thms = after_qed (the_single thms)
 in
-  Proof.theorem_i NONE after_qed' [goals'] ctxt
+  Proof.theorem NONE after_qed' [goals'] ctxt
 end
 
 
diff -r 2623a1987e1d -r c827275e530e src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/choice_specification.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -226,7 +226,7 @@
     in
       thy
       |> ProofContext.init
-      |> Proof.theorem_i NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
+      |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     end;
 
 
diff -r 2623a1987e1d -r c827275e530e src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/typedef.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -282,7 +282,7 @@
     val ((goal, goal_pat, typedef_result), lthy') =
       prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy;
     fun after_qed [[th]] = snd o typedef_result th;
-  in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] lthy' end;
+  in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
 
 in
 
diff -r 2623a1987e1d -r c827275e530e src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOLCF/Tools/pcpodef.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -328,7 +328,7 @@
       prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
     fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "cpodef_proof";
-  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 
 fun gen_pcpodef_proof prep_term prep_constraint
     ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
@@ -339,7 +339,7 @@
       prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
     fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "pcpodef_proof";
-  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 
 in
 
diff -r 2623a1987e1d -r c827275e530e src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/calculation.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -13,11 +13,11 @@
   val sym_add: attribute
   val sym_del: attribute
   val symmetric: attribute
-  val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
-  val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
-  val finally: (Facts.ref * Attrib.src list) list option -> bool ->
+  val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
+  val also_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
+  val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
+  val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
     Proof.state -> Proof.state Seq.seq
-  val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   val moreover: bool -> Proof.state -> Proof.state
   val ultimately: bool -> Proof.state -> Proof.state
 end;
@@ -148,10 +148,10 @@
         state |> maintain_calculation final calc))
   end;
 
-val also = calculate Proof.get_thmss false;
-val also_i = calculate (K I) false;
-val finally = calculate Proof.get_thmss true;
-val finally_i = calculate (K I) true;
+val also = calculate (K I) false;
+val also_cmd = calculate Proof.get_thmss_cmd false;
+val finally = calculate (K I) true;
+val finally_cmd = calculate Proof.get_thmss_cmd true;
 
 
 (* moreover and ultimately *)
diff -r 2623a1987e1d -r c827275e530e src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/class_target.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -163,7 +163,7 @@
       Symtab.empty
       |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
            Symtab.map_default (class, []) (insert (op =) tyco)) arities)
-             ((#arities o Sorts.rep_algebra) algebra);
+             (Sorts.arities_of algebra);
     val the_arities = these o Symtab.lookup arities;
     fun mk_arity class tyco =
       let
@@ -370,7 +370,7 @@
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed [[(mk_prop thy classrel, [])]]
+    |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
   end;
 
 in
@@ -539,7 +539,7 @@
   end;
 
 val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
-  Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
+  Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
 
 fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
@@ -595,7 +595,7 @@
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
+    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
   end;
 
 
diff -r 2623a1987e1d -r c827275e530e src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/element.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -283,10 +283,10 @@
 in
 
 fun witness_proof after_qed wit_propss =
-  gen_witness_proof (Proof.theorem_i NONE) (fn wits => fn _ => after_qed wits)
+  gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits)
     wit_propss [];
 
-val witness_proof_eqs = gen_witness_proof (Proof.theorem_i NONE);
+val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
 
 fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
   gen_witness_proof (fn after_qed' => fn propss =>
diff -r 2623a1987e1d -r c827275e530e src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -219,10 +219,10 @@
 fun goal opt_chain goal stmt int =
   opt_chain #> goal NONE (K I) stmt int;
 
-val have = goal I Proof.have;
-val hence = goal Proof.chain Proof.have;
-val show = goal I Proof.show;
-val thus = goal Proof.chain Proof.show;
+val have = goal I Proof.have_cmd;
+val hence = goal Proof.chain Proof.have_cmd;
+val show = goal I Proof.show_cmd;
+val thus = goal Proof.chain Proof.show_cmd;
 
 
 (* local endings *)
@@ -393,7 +393,7 @@
   let
     val thy = Toplevel.theory_of state;
     val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
-    val {classes, ...} = Sorts.rep_algebra algebra;
+    val classes = Sorts.classes_of algebra;
     fun entry (c, (i, (_, cs))) =
       (i, {name = Name_Space.extern space c, ID = c, parents = cs,
             dir = "", unfold = true, path = ""});
@@ -403,7 +403,7 @@
   in Present.display_graph gr end);
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  Thm_Deps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
+  Thm_Deps.thm_deps (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
 
 
 (* find unused theorems *)
@@ -437,12 +437,12 @@
 local
 
 fun string_of_stmts state args =
-  Proof.get_thmss state args
+  Proof.get_thmss_cmd state args
   |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
   |> Pretty.chunks2 |> Pretty.string_of;
 
 fun string_of_thms state args =
-  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
+  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args));
 
 fun string_of_prfs full state arg =
   Pretty.string_of
@@ -460,7 +460,7 @@
         end
     | SOME args => Pretty.chunks
         (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
-          (Proof.get_thmss state args)));
+          (Proof.get_thmss_cmd state args)));
 
 fun string_of_prop state s =
   let
diff -r 2623a1987e1d -r c827275e530e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -542,27 +542,27 @@
 val _ =
   OuterSyntax.command "from" "forward chaining from given facts"
     (K.tag_proof K.prf_chain)
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss)));
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
 
 val _ =
   OuterSyntax.command "with" "forward chaining from given and current facts"
     (K.tag_proof K.prf_chain)
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss)));
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
 
 val _ =
   OuterSyntax.command "note" "define facts"
     (K.tag_proof K.prf_decl)
-    (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss)));
+    (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
 
 val _ =
   OuterSyntax.command "using" "augment goal facts"
     (K.tag_proof K.prf_decl)
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using)));
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
 
 val _ =
   OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
     (K.tag_proof K.prf_decl)
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding)));
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
 
 
 (* proof context *)
@@ -570,17 +570,17 @@
 val _ =
   OuterSyntax.command "fix" "fix local variables (Skolem constants)"
     (K.tag_proof K.prf_asm)
-    (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
+    (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
 
 val _ =
   OuterSyntax.command "assume" "assume propositions"
     (K.tag_proof K.prf_asm)
-    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume)));
+    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
 
 val _ =
   OuterSyntax.command "presume" "assume propositions, to be established later"
     (K.tag_proof K.prf_asm)
-    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume)));
+    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
 
 val _ =
   OuterSyntax.command "def" "local definition"
@@ -588,24 +588,24 @@
     (P.and_list1
       (SpecParse.opt_thm_name ":" --
         ((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
-    >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
+    >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
 
 val _ =
   OuterSyntax.command "obtain" "generalized existence"
     (K.tag_proof K.prf_asm_goal)
     (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
-      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
+      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
 
 val _ =
   OuterSyntax.command "guess" "wild guessing (unstructured)"
     (K.tag_proof K.prf_asm_goal)
-    (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
+    (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
 
 val _ =
   OuterSyntax.command "let" "bind text variables"
     (K.tag_proof K.prf_decl)
     (P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
-      >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind)));
+      >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
 
 val case_spec =
   (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
@@ -614,7 +614,7 @@
 val _ =
   OuterSyntax.command "case" "invoke local context"
     (K.tag_proof K.prf_asm)
-    (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case)));
+    (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
 
 
 (* proof structure *)
@@ -711,12 +711,12 @@
 val _ =
   OuterSyntax.command "also" "combine calculation and current facts"
     (K.tag_proof K.prf_decl)
-    (calc_args >> (Toplevel.proofs' o Calculation.also));
+    (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
 
 val _ =
   OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
     (K.tag_proof K.prf_chain)
-    (calc_args >> (Toplevel.proofs' o Calculation.finally));
+    (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
 
 val _ =
   OuterSyntax.command "moreover" "augment calculation by current facts"
diff -r 2623a1987e1d -r c827275e530e src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/obtain.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -39,14 +39,14 @@
 signature OBTAIN =
 sig
   val thatN: string
-  val obtain: string -> (binding * string option * mixfix) list ->
+  val obtain: string -> (binding * typ option * mixfix) list ->
+    (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
+  val obtain_cmd: string -> (binding * string option * mixfix) list ->
     (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
-  val obtain_i: string -> (binding * typ option * mixfix) list ->
-    (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
     ((string * cterm) list * thm list) * Proof.context
-  val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
-  val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+  val guess: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+  val guess_cmd: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
 end;
 
 structure Obtain: OBTAIN =
@@ -148,26 +148,26 @@
     fun after_qed _ =
       Proof.local_qed (NONE, false)
       #> `Proof.the_fact #-> (fn rule =>
-        Proof.fix_i vars
-        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
+        Proof.fix vars
+        #> Proof.assm (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
   in
     state
     |> Proof.enter_forward
-    |> Proof.have_i NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
+    |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
-    |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
-    |> Proof.assume_i
+    |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
+    |> Proof.assume
       [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
-    ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
+    ||> Proof.show NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
     |-> Proof.refine_insert
   end;
 
 in
 
-val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
-val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
+val obtain = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
+val obtain_cmd = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
 
 end;
 
@@ -290,8 +290,8 @@
       in
         state'
         |> Proof.map_context (K ctxt')
-        |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
-        |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
+        |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
+        |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
           (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
         |> Proof.bind_terms Auto_Bind.no_facts
       end;
@@ -307,7 +307,7 @@
     state
     |> Proof.enter_forward
     |> Proof.begin_block
-    |> Proof.fix_i [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
+    |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
     |> Proof.local_goal print_result (K I) (apsnd (rpair I))
       "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
@@ -316,8 +316,8 @@
 
 in
 
-val guess = gen_guess ProofContext.read_vars;
-val guess_i = gen_guess ProofContext.cert_vars;
+val guess = gen_guess ProofContext.cert_vars;
+val guess_cmd = gen_guess ProofContext.read_vars;
 
 end;
 
diff -r 2623a1987e1d -r c827275e530e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/proof.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -41,37 +41,35 @@
   val raw_goal: state -> {context: context, facts: thm list, goal: thm}
   val goal: state -> {context: context, facts: thm list, goal: thm}
   val simple_goal: state -> {context: context, goal: thm}
-  val match_bind: (string list * string) list -> state -> state
-  val match_bind_i: (term list * term) list -> state -> state
-  val let_bind: (string list * string) list -> state -> state
-  val let_bind_i: (term list * term) list -> state -> state
-  val fix: (binding * string option * mixfix) list -> state -> state
-  val fix_i: (binding * typ option * mixfix) list -> state -> state
+  val let_bind: (term list * term) list -> state -> state
+  val let_bind_cmd: (string list * string) list -> state -> state
+  val fix: (binding * typ option * mixfix) list -> state -> state
+  val fix_cmd: (binding * string option * mixfix) list -> state -> state
   val assm: Assumption.export ->
+    (Thm.binding * (term * term list) list) list -> state -> state
+  val assm_cmd: Assumption.export ->
     (Attrib.binding * (string * string list) list) list -> state -> state
-  val assm_i: Assumption.export ->
-    (Thm.binding * (term * term list) list) list -> state -> state
-  val assume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val assume_i: (Thm.binding * (term * term list) list) list -> state -> state
-  val presume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val presume_i: (Thm.binding * (term * term list) list) list -> state -> state
-  val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
-  val def_i: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
+  val assume: (Thm.binding * (term * term list) list) list -> state -> state
+  val assume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
+  val presume: (Thm.binding * (term * term list) list) list -> state -> state
+  val presume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
+  val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
+  val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
-  val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
-  val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
-  val note_thmss_i: (Thm.binding * (thm list * attribute list) list) list -> state -> state
-  val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
-  val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
-  val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
-  val with_thmss_i: ((thm list * attribute list) list) list -> state -> state
-  val using: ((Facts.ref * Attrib.src list) list) list -> state -> state
-  val using_i: ((thm list * attribute list) list) list -> state -> state
-  val unfolding: ((Facts.ref * Attrib.src list) list) list -> state -> state
-  val unfolding_i: ((thm list * attribute list) list) list -> state -> state
-  val invoke_case: string * string option list * Attrib.src list -> state -> state
-  val invoke_case_i: string * string option list * attribute list -> state -> state
+  val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list
+  val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
+  val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
+  val from_thmss: ((thm list * attribute list) list) list -> state -> state
+  val from_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val with_thmss: ((thm list * attribute list) list) list -> state -> state
+  val with_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val using: ((thm list * attribute list) list) list -> state -> state
+  val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val unfolding: ((thm list * attribute list) list) list -> state -> state
+  val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val invoke_case: string * string option list * attribute list -> state -> state
+  val invoke_case_cmd: string * string option list * Attrib.src list -> state -> state
   val begin_block: state -> state
   val next_block: state -> state
   val end_block: state -> state
@@ -87,9 +85,9 @@
     ((binding * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
+    (term * term list) list list -> context -> state
+  val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
     (string * string list) list list -> context -> state
-  val theorem_i: Method.text option -> (thm list list -> context -> context) ->
-    (term * term list) list list -> context -> state
   val global_qed: Method.text option * bool -> state -> context
   val local_terminal_proof: Method.text * Method.text option -> state -> state
   val local_default_proof: state -> state
@@ -102,13 +100,13 @@
   val global_skip_proof: bool -> state -> context
   val global_done_proof: state -> context
   val have: Method.text option -> (thm list list -> state -> state) ->
+    (Thm.binding * (term * term list) list) list -> bool -> state -> state
+  val have_cmd: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
-  val have_i: Method.text option -> (thm list list -> state -> state) ->
-    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val show: Method.text option -> (thm list list -> state -> state) ->
+    (Thm.binding * (term * term list) list) list -> bool -> state -> state
+  val show_cmd: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
-  val show_i: Method.text option -> (thm list list -> state -> state) ->
-    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val schematic_goal: state -> bool
   val is_relevant: state -> bool
   val local_future_proof: (state -> ('a * state) Future.future) ->
@@ -523,22 +521,20 @@
 
 (** context elements **)
 
-(* bindings *)
+(* let bindings *)
 
 local
 
 fun gen_bind bind args state =
   state
   |> assert_forward
-  |> map_context (bind args #> snd)
+  |> map_context (bind true args #> snd)
   |> put_facts NONE;
 
 in
 
-val match_bind = gen_bind (ProofContext.match_bind false);
-val match_bind_i = gen_bind (ProofContext.match_bind_i false);
-val let_bind = gen_bind (ProofContext.match_bind true);
-val let_bind_i = gen_bind (ProofContext.match_bind_i true);
+val let_bind = gen_bind ProofContext.match_bind_i;
+val let_bind_cmd = gen_bind ProofContext.match_bind;
 
 end;
 
@@ -554,8 +550,8 @@
 
 in
 
-val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
-val fix_i = gen_fix (K I);
+val fix = gen_fix (K I);
+val fix_cmd = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
 
 end;
 
@@ -572,12 +568,12 @@
 
 in
 
-val assm      = gen_assume ProofContext.add_assms Attrib.attribute;
-val assm_i    = gen_assume ProofContext.add_assms_i (K I);
-val assume    = assm Assumption.assume_export;
-val assume_i  = assm_i Assumption.assume_export;
-val presume   = assm Assumption.presume_export;
-val presume_i = assm_i Assumption.presume_export;
+val assm = gen_assume ProofContext.add_assms_i (K I);
+val assm_cmd = gen_assume ProofContext.add_assms Attrib.attribute;
+val assume = assm Assumption.assume_export;
+val assume_cmd = assm_cmd Assumption.assume_export;
+val presume = assm Assumption.presume_export;
+val presume_cmd = assm_cmd Assumption.presume_export;
 
 end;
 
@@ -605,8 +601,8 @@
 
 in
 
-val def = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
-val def_i = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
+val def = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
+val def_cmd = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
 
 end;
 
@@ -646,18 +642,18 @@
 
 in
 
-val note_thmss = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
-val note_thmss_i = gen_thmss (K []) I #2 (K I) (K I);
+val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
+val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
 
-val from_thmss = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
-val from_thmss_i = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
+val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
+val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
 
-val with_thmss = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
-val with_thmss_i = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
 
 val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
 
-fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
+fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state);
 
 end;
 
@@ -686,10 +682,10 @@
 
 in
 
-val using = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
-val using_i = gen_using append_using (K (K I)) (K I) (K I);
-val unfolding = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
-val unfolding_i = gen_using unfold_using unfold_goals (K I) (K I);
+val using = gen_using append_using (K (K I)) (K I) (K I);
+val using_cmd = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
+val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
+val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
 
 end;
 
@@ -709,15 +705,15 @@
     val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
   in
     state'
-    |> assume_i assumptions
+    |> assume assumptions
     |> bind_terms Auto_Bind.no_facts
-    |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
+    |> `the_facts |-> (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])])
   end;
 
 in
 
-val invoke_case = gen_invoke_case Attrib.attribute;
-val invoke_case_i = gen_invoke_case (K I);
+val invoke_case = gen_invoke_case (K I);
+val invoke_case_cmd = gen_invoke_case Attrib.attribute;
 
 end;
 
@@ -790,15 +786,16 @@
 
 local
 
-fun implicit_vars dest add props =
+val is_var =
+  can (dest_TVar o Logic.dest_type o Logic.dest_term) orf
+  can (dest_Var o Logic.dest_term);
+
+fun implicit_vars props =
   let
-    val (explicit_vars, props') = take_prefix (can dest) props |>> map dest;
-    val vars = rev (subtract (op =) explicit_vars (fold add props []));
-    val _ =
-      if null vars then ()
-      else warning ("Goal statement contains unbound schematic variable(s): " ^
-        commas_quote (map (Term.string_of_vname o fst) vars));
-  in (rev vars, props') end;
+    val (var_props, props') = take_prefix is_var props;
+    val explicit_vars = fold Term.add_vars var_props [];
+    val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
+  in map (Logic.mk_term o Var) vars end;
 
 fun refine_terms n =
   refine (Method.Basic (K (RAW_METHOD
@@ -823,11 +820,8 @@
       |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp)));
     val props = flat propss;
 
-    val (_, props') =
-      implicit_vars (dest_TVar o Logic.dest_type o Logic.dest_term) Term.add_tvars props;
-    val (vars, _) = implicit_vars (dest_Var o Logic.dest_term) Term.add_vars props';
-
-    val propss' = map (Logic.mk_term o Var) vars :: propss;
+    val vars = implicit_vars props;
+    val propss' = vars :: propss;
     val goal_propss = filter_out null propss';
     val goal =
       cert (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss))
@@ -903,8 +897,8 @@
   init ctxt
   |> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
 
-val theorem = global_goal ProofContext.bind_propp_schematic;
-val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
+val theorem = global_goal ProofContext.bind_propp_schematic_i;
+val theorem_cmd = global_goal ProofContext.bind_propp_schematic;
 
 fun global_qeds txt =
   end_proof true txt
@@ -976,10 +970,10 @@
 
 in
 
-val have = gen_have Attrib.attribute ProofContext.bind_propp;
-val have_i = gen_have (K I) ProofContext.bind_propp_i;
-val show = gen_show Attrib.attribute ProofContext.bind_propp;
-val show_i = gen_show (K I) ProofContext.bind_propp_i;
+val have = gen_have (K I) ProofContext.bind_propp_i;
+val have_cmd = gen_have Attrib.attribute ProofContext.bind_propp;
+val show = gen_show (K I) ProofContext.bind_propp_i;
+val show_cmd = gen_show Attrib.attribute ProofContext.bind_propp;
 
 end;
 
diff -r 2623a1987e1d -r c827275e530e src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/specification.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -403,7 +403,7 @@
     goal_ctxt
     |> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
     |> snd
-    |> Proof.theorem_i before_qed after_qed' (map snd stmt)
+    |> Proof.theorem before_qed after_qed' (map snd stmt)
     |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
     |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
         error "Illegal schematic goal statement")
diff -r 2623a1987e1d -r c827275e530e src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/ML/ml_thms.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -64,7 +64,7 @@
         fun after_qed res goal_ctxt =
           put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt;
         val ctxt' = ctxt
-          |> Proof.theorem_i NONE after_qed propss
+          |> Proof.theorem NONE after_qed propss
           |> Proof.global_terminal_proof methods;
         val (a, background') = background
           |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
diff -r 2623a1987e1d -r c827275e530e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Thy/thy_output.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -574,7 +574,7 @@
       val prop_src =
         (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
       val _ = context
-        |> Proof.theorem_i NONE (K I) [[(prop, [])]]
+        |> Proof.theorem NONE (K I) [[(prop, [])]]
         |> Proof.global_terminal_proof methods;
     in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
 
diff -r 2623a1987e1d -r c827275e530e src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/axclass.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -13,8 +13,8 @@
   val add_arity: thm -> theory -> theory
   val prove_classrel: class * class -> tactic -> theory -> theory
   val prove_arity: string * sort list * sort -> tactic -> theory -> theory
-  val get_info: theory -> class ->
-    {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
+  type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
+  val get_info: theory -> class -> info
   val class_intros: theory -> thm list
   val class_of_param: theory -> string -> class option
   val cert_classrel: theory -> class * class -> class * class
@@ -37,8 +37,6 @@
   val param_of_inst: theory -> string * string -> string
   val inst_of_param: theory -> string -> (string * string) option
   val thynames_of_arity: theory -> class * string -> string list
-  val introN: string
-  val axiomsN: string
 end;
 
 structure AxClass: AX_CLASS =
@@ -46,6 +44,18 @@
 
 (** theory data **)
 
+(* axclass info *)
+
+type info =
+ {def: thm,
+  intro: thm,
+  axioms: thm list,
+  params: (string * typ) list};
+
+fun make_axclass (def, intro, axioms, params): info =
+  {def = def, intro = intro, axioms = axioms, params = params};
+
+
 (* class parameters (canonical order) *)
 
 type param = string * class;
@@ -57,188 +67,265 @@
       " for " ^ Pretty.string_of_sort pp [c] ^
       (if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c'])));
 
-fun merge_params _ ([], qs) = qs
-  | merge_params pp (ps, qs) =
-      fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps;
+
+(* setup data *)
+
+datatype data = Data of
+ {axclasses: info Symtab.table,
+  params: param list,
+  proven_classrels: (thm * proof) Symreltab.table,
+  proven_arities: ((class * sort list) * ((thm * string) * proof)) list Symtab.table,
+    (*arity theorems with theory name*)
+  inst_params:
+    (string * thm) Symtab.table Symtab.table *
+      (*constant name ~> type constructor ~> (constant name, equation)*)
+    (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*),
+  diff_merge_classrels: (class * class) list};
+
+fun make_data
+    (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =
+  Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels,
+    proven_arities = proven_arities, inst_params = inst_params,
+    diff_merge_classrels = diff_merge_classrels};
+
+structure Data = Theory_Data_PP
+(
+  type T = data;
+  val empty =
+    make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty), []);
+  val extend = I;
+  fun merge pp
+      (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1,
+        proven_arities = proven_arities1, inst_params = inst_params1,
+        diff_merge_classrels = diff_merge_classrels1},
+       Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2,
+        proven_arities = proven_arities2, inst_params = inst_params2,
+        diff_merge_classrels = diff_merge_classrels2}) =
+    let
+      val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
+      val params' =
+        if null params1 then params2
+        else fold_rev (fn q => if member (op =) params1 q then I else add_param pp q) params2 params1;
+
+      (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
+      val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
+      val proven_arities' =
+        Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2);
+
+      val classrels1 = Symreltab.keys proven_classrels1;
+      val classrels2 = Symreltab.keys proven_classrels2;
+      val diff_merge_classrels' =
+        subtract (op =) classrels1 classrels2 @
+        subtract (op =) classrels2 classrels1 @
+        diff_merge_classrels1 @ diff_merge_classrels2;
+
+      val inst_params' =
+        (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
+          Symtab.merge (K true) (#2 inst_params1, #2 inst_params2));
+    in
+      make_data (axclasses', params', proven_classrels', proven_arities', inst_params',
+        diff_merge_classrels')
+    end;
+);
+
+fun map_data f =
+  Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels} =>
+    make_data (f (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels)));
+
+fun map_axclasses f =
+  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+    (f axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
+
+fun map_params f =
+  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+    (axclasses, f params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
+
+fun map_proven_classrels f =
+  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+    (axclasses, params, f proven_classrels, proven_arities, inst_params, diff_merge_classrels));
+
+fun map_proven_arities f =
+  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+    (axclasses, params, proven_classrels, f proven_arities, inst_params, diff_merge_classrels));
+
+fun map_inst_params f =
+  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+    (axclasses, params, proven_classrels, proven_arities, f inst_params, diff_merge_classrels));
+
+val clear_diff_merge_classrels =
+  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, _) =>
+    (axclasses, params, proven_classrels, proven_arities, inst_params, []));
+
+val rep_data = Data.get #> (fn Data args => args);
+
+val axclasses_of = #axclasses o rep_data;
+val params_of = #params o rep_data;
+val proven_classrels_of = #proven_classrels o rep_data;
+val proven_arities_of = #proven_arities o rep_data;
+val inst_params_of = #inst_params o rep_data;
+val diff_merge_classrels_of = #diff_merge_classrels o rep_data;
 
 
-(* axclasses *)
-
-val introN = "intro";
-val superN = "super";
-val axiomsN = "axioms";
+(* maintain axclasses *)
 
-datatype axclass = AxClass of
- {def: thm,
-  intro: thm,
-  axioms: thm list,
-  params: (string * typ) list};
+fun get_info thy c =
+  (case Symtab.lookup (axclasses_of thy) c of
+    SOME info => info
+  | NONE => error ("No such axclass: " ^ quote c));
 
-type axclasses = axclass Symtab.table * param list;
-
-fun make_axclass ((def, intro, axioms), params) = AxClass
-  {def = def, intro = intro, axioms = axioms, params = params};
-
-fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses =
-  (Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2));
+fun class_intros thy =
+  let
+    fun add_intro c = (case try (get_info thy) c of SOME {intro, ...} => cons intro | _ => I);
+    val classes = Sign.all_classes thy;
+  in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
 
 
-(* instances *)
+(* maintain params *)
+
+fun all_params_of thy S =
+  let val params = params_of thy;
+  in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end;
+
+fun class_of_param thy = AList.lookup (op =) (params_of thy);
+
+
+(* maintain instances *)
 
 val classrel_prefix = "classrel_";
 val arity_prefix = "arity_";
 
-type instances =
-  ((class * class) * thm) list *  (*classrel theorems*)
-  ((class * sort list) * (thm * string)) list Symtab.table;  (*arity theorems with theory name*)
-
-fun merge_instances ((classrel1, arities1): instances, (classrel2, arities2)) =
- (merge (eq_fst op =) (classrel1, classrel2),
-  Symtab.join (K (merge (eq_fst op =))) (arities1, arities2));
-
-
-(* instance parameters *)
-
-type inst_params =
-  (string * thm) Symtab.table Symtab.table
-    (*constant name ~> type constructor ~> (constant name, equation)*)
-  * (string * string) Symtab.table; (*constant name ~> (constant name, type constructor)*)
-
-fun merge_inst_params ((const_param1, param_const1), (const_param2, param_const2)) =
-  (Symtab.join  (K (Symtab.merge (K true))) (const_param1, const_param2),
-    Symtab.merge (K true) (param_const1, param_const2));
-
-
-(* setup data *)
-
-structure AxClassData = Theory_Data_PP
-(
-  type T = axclasses * (instances * inst_params);
-  val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
-  val extend = I;
-  fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
-    (merge_axclasses pp (axclasses1, axclasses2),
-      (merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2)));
-);
-
-
-(* maintain axclasses *)
-
-val get_axclasses = #1 o AxClassData.get;
-val map_axclasses = AxClassData.map o apfst;
-
-val lookup_def = Symtab.lookup o #1 o get_axclasses;
-
-fun get_info thy c =
-  (case lookup_def thy c of
-    SOME (AxClass info) => info
-  | NONE => error ("No such axclass: " ^ quote c));
-
-fun class_intros thy =
-  let
-    fun add_intro c =
-      (case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I);
-    val classes = Sign.all_classes thy;
-  in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
-
-
-fun get_params thy pred =
-  let val params = #2 (get_axclasses thy);
-  in fold (fn (x, c) => if pred c then cons x else I) params [] end;
-
-fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
-
-fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy));
-
-
-(* maintain instances *)
-
 fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
 
-val get_instances = #1 o #2 o AxClassData.get;
-val map_instances = AxClassData.map o apsnd o apfst;
-
 
 fun the_classrel thy (c1, c2) =
-  (case AList.lookup (op =) (#1 (get_instances thy)) (c1, c2) of
-    SOME th => Thm.transfer thy th
+  (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
+    SOME classrel => classrel
   | NONE => error ("Unproven class relation " ^
       Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
 
-fun put_classrel arg = map_instances (fn (classrel, arities) =>
-  (insert (eq_fst op =) arg classrel, arities));
+fun the_classrel_thm thy = Thm.transfer thy o #1 o the_classrel thy;
+fun the_classrel_prf thy = #2 o the_classrel thy;
+
+fun put_trancl_classrel ((c1, c2), th) thy =
+  let
+    val cert = Thm.cterm_of thy;
+    val certT = Thm.ctyp_of thy;
+
+    val classes = Sorts.classes_of (Sign.classes_of thy);
+    val classrels = proven_classrels_of thy;
+
+    fun reflcl_classrel (c1', c2') =
+      if c1' = c2'
+      then Thm.trivial (cert (Logic.mk_of_class (TVar ((Name.aT, 0), []), c1')))
+      else the_classrel_thm thy (c1', c2');
+    fun gen_classrel (c1_pred, c2_succ) =
+      let
+        val th' = ((reflcl_classrel (c1_pred, c1) RS th) RS reflcl_classrel (c2, c2_succ))
+          |> Drule.instantiate' [SOME (certT (TVar ((Name.aT, 0), [])))] []
+          |> Thm.close_derivation;
+        val prf' = Thm.proof_of th';
+      in ((c1_pred, c2_succ), (th', prf')) end;
+
+    val new_classrels =
+      Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
+      |> filter_out (Symreltab.defined classrels)
+      |> map gen_classrel;
+    val needed = not (null new_classrels);
+  in
+    (needed,
+      if needed then map_proven_classrels (fold Symreltab.update new_classrels) thy
+      else thy)
+  end;
+
+fun complete_classrels thy =
+  let
+    val classrels = proven_classrels_of thy;
+    val diff_merge_classrels = diff_merge_classrels_of thy;
+    val (needed, thy') = (false, thy) |>
+      fold (fn c12 => fn (needed, thy) =>
+          put_trancl_classrel (c12, Symreltab.lookup classrels c12 |> the |> #1) thy
+          |>> (fn b => needed orelse b))
+        diff_merge_classrels;
+  in
+    if null diff_merge_classrels then NONE
+    else SOME (clear_diff_merge_classrels thy')
+  end;
 
 
 fun the_arity thy a (c, Ss) =
-  (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of
-    SOME (th, _) => Thm.transfer thy th
+  (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
+    SOME arity => arity
   | NONE => error ("Unproven type arity " ^
       Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
 
+fun the_arity_thm thy a c_Ss = the_arity thy a c_Ss |> #1 |> #1 |> Thm.transfer thy;
+fun the_arity_prf thy a c_Ss = the_arity thy a c_Ss |> #2;
+
 fun thynames_of_arity thy (c, a) =
-  Symtab.lookup_list (#2 (get_instances thy)) a
-  |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE)
+  Symtab.lookup_list (proven_arities_of thy) a
+  |> map_filter (fn ((c', _), ((_, name),_)) => if c = c' then SOME name else NONE)
   |> rev;
 
-fun insert_arity_completions thy (t, ((c, Ss), (th, thy_name))) arities =
+fun insert_arity_completions thy (t, ((c, Ss), ((th, thy_name), _))) arities =
   let
     val algebra = Sign.classes_of thy;
     val super_class_completions =
       Sign.super_classes thy c
       |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
           andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
-    val completions = map (fn c1 => (Sorts.classrel_derivation algebra
-      (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
-        |> Thm.close_derivation, c1)) super_class_completions;
-    val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), (th1, thy_name))))
+    val names_and_Ss = Name.names Name.context Name.aT (map (K []) Ss);
+    val completions = super_class_completions |> map (fn c1 =>
+      let
+        val th1 = (th RS the_classrel_thm thy (c, c1))
+          |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names_and_Ss) []
+          |> Thm.close_derivation;
+        val prf1 = Thm.proof_of th1;
+      in (((th1, thy_name), prf1), c1) end);
+    val arities' = fold (fn (th_thy_prf1, c1) => Symtab.cons_list (t, ((c1, Ss), th_thy_prf1)))
       completions arities;
   in (null completions, arities') end;
 
 fun put_arity ((t, Ss, c), th) thy =
   let
-    val arity' = (t, ((c, Ss), (th, Context.theory_name thy)));
+    val arity' = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th)));
   in
     thy
-    |> map_instances (fn (classrel, arities) => (classrel,
-      arities
-      |> Symtab.insert_list (eq_fst op =) arity'
-      |> insert_arity_completions thy arity'
-      |> snd))
+    |> map_proven_arities
+      (Symtab.insert_list (eq_fst op =) arity' #>
+        insert_arity_completions thy arity' #> snd)
   end;
 
 fun complete_arities thy =
   let
-    val arities = snd (get_instances thy);
+    val arities = proven_arities_of thy;
     val (finished, arities') = arities
       |> fold_map (insert_arity_completions thy) (Symtab.dest_list arities);
   in
-    if forall I finished then NONE
-    else SOME (thy |> map_instances (fn (classrel, _) => (classrel, arities')))
+    if forall I finished
+    then NONE
+    else SOME (map_proven_arities (K arities') thy)
   end;
 
-val _ = Context.>> (Context.map_theory (Theory.at_begin complete_arities));
+val _ = Context.>> (Context.map_theory
+  (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities));
 
 
 (* maintain instance parameters *)
 
-val get_inst_params = #2 o #2 o AxClassData.get;
-val map_inst_params = AxClassData.map o apsnd o apsnd;
+fun get_inst_param thy (c, tyco) =
+  (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (inst_params_of thy)) c)) tyco of
+    SOME c' => c'
+  | NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco));
 
-fun get_inst_param thy (c, tyco) =
-  case Symtab.lookup ((the_default Symtab.empty o Symtab.lookup (fst (get_inst_params thy))) c) tyco
-   of SOME c' => c'
-    | NONE => error ("No instance parameter for constant " ^ quote c
-        ^ " on type constructor " ^ quote tyco);
-
-fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
-      o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
+fun add_inst_param (c, tyco) inst =
+  (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
   #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
 
-val inst_of_param = Symtab.lookup o snd o get_inst_params;
+val inst_of_param = Symtab.lookup o #2 o inst_params_of;
 val param_of_inst = fst oo get_inst_param;
 
-fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
-  (get_inst_params thy) [];
+fun inst_thms thy =
+  Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) [];
 
 fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts);
 
@@ -248,18 +335,20 @@
 fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
 fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
 
-fun lookup_inst_param consts params (c, T) = case get_inst_tyco consts (c, T)
- of SOME tyco => AList.lookup (op =) params (c, tyco)
-  | NONE => NONE;
+fun lookup_inst_param consts params (c, T) =
+  (case get_inst_tyco consts (c, T) of
+    SOME tyco => AList.lookup (op =) params (c, tyco)
+  | NONE => NONE);
 
 fun unoverload_const thy (c_ty as (c, _)) =
-  if is_some (class_of_param thy c)
-  then case get_inst_tyco (Sign.consts_of thy) c_ty
-   of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
-    | NONE => c
+  if is_some (class_of_param thy c) then
+    (case get_inst_tyco (Sign.consts_of thy) c_ty of
+      SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
+    | NONE => c)
   else c;
 
 
+
 (** instances **)
 
 (* class relations *)
@@ -331,6 +420,8 @@
 
 (* primitive rules *)
 
+val shyps_topped = forall null o #shyps o Thm.rep_thm;
+
 fun add_classrel raw_th thy =
   let
     val th = Thm.strip_shyps (Thm.transfer thy raw_th);
@@ -338,10 +429,14 @@
     fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
     val rel = Logic.dest_classrel prop handle TERM _ => err ();
     val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
+    val th' = th
+      |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [c1])))] []
+      |> Thm.unconstrain_allTs;
+    val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain";
   in
     thy
     |> Sign.primitive_classrel (c1, c2)
-    |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th))
+    |> (snd oo put_trancl_classrel) ((c1, c2), th')
     |> perhaps complete_arities
   end;
 
@@ -351,17 +446,22 @@
     val prop = Thm.plain_prop_of th;
     fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
     val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
-    val T = Type (t, map TFree (Name.names Name.context Name.aT Ss));
+    val names = Name.names Name.context Name.aT Ss;
+    val T = Type (t, map TFree names);
     val missing_params = Sign.complete_sort thy [c]
       |> maps (these o Option.map #params o try (get_info thy))
       |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
       |> (map o apsnd o map_atyps) (K T);
     val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
+    val th' = th
+      |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names) []
+      |> Thm.unconstrain_allTs;
+    val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
   in
     thy
     |> fold (snd oo declare_overloaded) missing_params
     |> Sign.primitive_arity (t, Ss, [c])
-    |> put_arity ((t, Ss, c), Thm.close_derivation (Drule.unconstrainTs th))
+    |> put_arity ((t, Ss, c), th')
   end;
 
 
@@ -483,25 +583,24 @@
       def_thy
       |> Sign.qualified_path true bconst
       |> PureThy.note_thmss ""
-        [((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]),
-         ((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]),
-         ((Binding.name axiomsN, []),
+        [((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]),
+         ((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]),
+         ((Binding.name "axioms", []),
            [(map (fn th => Drule.export_without_context (class_triv RS th)) raw_axioms, [])])]
       ||> Sign.restore_naming def_thy;
 
 
     (* result *)
 
-    val axclass = make_axclass ((def, intro, axioms), params);
+    val axclass = make_axclass (def, intro, axioms, params);
     val result_thy =
       facts_thy
-      |> fold put_classrel (map (pair class) super ~~ classrel)
+      |> fold (snd oo put_trancl_classrel) (map (pair class) super ~~ classrel)
       |> Sign.qualified_path false bconst
       |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
       |> Sign.restore_naming facts_thy
-      |> map_axclasses (fn (axclasses, parameters) =>
-        (Symtab.update (class, axclass) axclasses,
-          fold (fn (x, _) => add_param pp (x, class)) params parameters));
+      |> map_axclasses (Symtab.update (class, axclass))
+      |> map_params (fold (fn (x, _) => add_param pp (x, class)) params);
 
   in (class, result_thy) end;
 
diff -r 2623a1987e1d -r c827275e530e src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/display.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -182,7 +182,8 @@
     val extern_const = Name_Space.extern (#1 constants);
     val {classes, default, types, ...} = Type.rep_tsig tsig;
     val (class_space, class_algebra) = classes;
-    val {classes, arities} = Sorts.rep_algebra class_algebra;
+    val classes = Sorts.classes_of class_algebra;
+    val arities = Sorts.arities_of class_algebra;
 
     val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
     val tdecls = Name_Space.dest_table types;
diff -r 2623a1987e1d -r c827275e530e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/drule.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -106,7 +106,6 @@
   val dummy_thm: thm
   val sort_constraintI: thm
   val sort_constraint_eq: thm
-  val unconstrainTs: thm -> thm
   val with_subgoal: int -> (thm -> thm) -> thm -> thm
   val comp_no_flatten: thm * int -> int -> thm -> thm
   val rename_bvars: (string * string) list -> thm -> thm
@@ -204,12 +203,6 @@
 
 (** Standardization of rules **)
 
-(* type classes and sorts *)
-
-fun unconstrainTs th =
-  fold (Thm.unconstrainT o Thm.ctyp_of (Thm.theory_of_thm th) o TVar)
-    (Thm.fold_terms Term.add_tvars th []) th;
-
 (*Generalization over a list of variables*)
 val forall_intr_list = fold_rev forall_intr;
 
diff -r 2623a1987e1d -r c827275e530e src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/sorts.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -25,9 +25,8 @@
   val insert_term: term -> sort OrdList.T -> sort OrdList.T
   val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
   type algebra
-  val rep_algebra: algebra ->
-   {classes: serial Graph.T,
-    arities: (class * (class * sort list)) list Symtab.table}
+  val classes_of: algebra -> serial Graph.T
+  val arities_of: algebra -> (class * (class * sort list)) list Symtab.table
   val all_classes: algebra -> class list
   val super_classes: algebra -> class -> class list
   val class_less: algebra -> class * class -> bool
@@ -116,10 +115,8 @@
  {classes: serial Graph.T,
   arities: (class * (class * sort list)) list Symtab.table};
 
-fun rep_algebra (Algebra args) = args;
-
-val classes_of = #classes o rep_algebra;
-val arities_of = #arities o rep_algebra;
+fun classes_of (Algebra {classes, ...}) = classes;
+fun arities_of (Algebra {arities, ...}) = arities;
 
 fun make_algebra (classes, arities) =
   Algebra {classes = classes, arities = arities};
diff -r 2623a1987e1d -r c827275e530e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/thm.ML	Sun Apr 25 23:26:40 2010 +0200
@@ -92,8 +92,6 @@
   val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
   val trivial: cterm -> thm
-  val of_class: ctyp * class -> thm
-  val unconstrainT: ctyp -> thm -> thm
   val dest_state: thm * int -> (term * term) list * term list * term * term
   val lift_rule: cterm -> thm -> thm
   val incr_indexes: int -> thm -> thm
@@ -139,6 +137,9 @@
   val adjust_maxidx_thm: int -> thm -> thm
   val varifyT_global: thm -> thm
   val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
+  val of_class: ctyp * class -> thm
+  val unconstrainT: ctyp -> thm -> thm
+  val unconstrain_allTs: thm -> thm
   val freezeT: thm -> thm
   val assumption: int -> thm -> thm Seq.seq
   val eq_assumption: int -> thm -> thm
@@ -1240,6 +1241,11 @@
       prop = Logic.list_implies (constraints, unconstrain prop)})
   end;
 
+fun unconstrain_allTs th =
+  fold (unconstrainT o ctyp_of (theory_of_thm th) o TVar)
+    (fold_terms Term.add_tvars th []) th;
+
+
 (* Replace all TFrees not fixed or in the hyps by new TVars *)
 fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
   let