clarified modules;
tuned signature;

--- a/src/Pure/Isar/proof.ML	Fri Oct 23 16:09:06 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Oct 23 17:17:11 2015 +0200
@@ -501,7 +501,7 @@
       (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
         handle THM _ => err_lost ())
       |> Drule.flexflex_unique (SOME ctxt)
-      |> Thm.check_shyps ctxt (Variable.sorts_of ctxt)
+      |> Thm.check_shyps ctxt
       |> Thm.check_hyps (Context.Proof ctxt);
 
     val goal_propss = filter_out null propss;
@@ -947,7 +947,7 @@
     val goal =
       Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
       |> Thm.cterm_of goal_ctxt
-      |> Thm.weaken_sorts (Variable.sorts_of goal_ctxt);
+      |> Thm.weaken_sorts' goal_ctxt;
     val statement = ((kind, pos), propss', Thm.term_of goal);
 
     val after_qed' = after_qed |>> (fn after_local => fn results =>

--- a/src/Pure/goal.ML	Fri Oct 23 16:09:06 2015 +0200
+++ b/src/Pure/goal.ML	Fri Oct 23 17:17:11 2015 +0200
@@ -137,7 +137,7 @@
     val global_prop =
       Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))
       |> Thm.cterm_of ctxt
-      |> Thm.weaken_sorts (Variable.sorts_of ctxt);
+      |> Thm.weaken_sorts' ctxt;
     val global_result = result |> Future.map
       (Drule.flexflex_unique (SOME ctxt) #>
         Thm.adjust_maxidx_thm ~1 #>
@@ -196,9 +196,8 @@
       |> fold Variable.declare_term (asms @ props)
       |> Assumption.add_assumes casms
       ||> Variable.set_body true;
-    val sorts = Variable.sorts_of ctxt';
 
-    val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops);
+    val stmt = Thm.weaken_sorts' ctxt' (Conjunction.mk_conjunction_balanced cprops);
 
     fun tac' args st =
       if skip then ALLGOALS (Skip_Proof.cheat_tac ctxt) st before Skip_Proof.report ctxt
@@ -214,7 +213,7 @@
             val res =
               (finish ctxt' st
                 |> Drule.flexflex_unique (SOME ctxt')
-                |> Thm.check_shyps ctxt' sorts
+                |> Thm.check_shyps ctxt'
                 |> Thm.check_hyps (Context.Proof ctxt'))
               handle THM (msg, _, _) => err msg | ERROR msg => err msg;
           in

--- a/src/Pure/more_thm.ML	Fri Oct 23 16:09:06 2015 +0200
+++ b/src/Pure/more_thm.ML	Fri Oct 23 17:17:11 2015 +0200
@@ -48,7 +48,6 @@
   val equiv_thm: theory -> thm * thm -> bool
   val class_triv: theory -> class -> thm
   val of_sort: ctyp * sort -> thm list
-  val check_shyps: Proof.context -> sort list -> thm -> thm
   val is_dummy: thm -> bool
   val plain_prop_of: thm -> term
   val add_thm: thm -> thm list -> thm list
@@ -63,6 +62,9 @@
   val restore_hyps: Proof.context -> Proof.context -> Proof.context
   val undeclared_hyps: Context.generic -> thm -> term list
   val check_hyps: Context.generic -> thm -> thm
+  val declare_term_sorts: term -> Proof.context -> Proof.context
+  val check_shyps: Proof.context -> thm -> thm
+  val weaken_sorts': Proof.context -> cterm -> cterm
   val elim_implies: thm -> thm -> thm
   val forall_intr_name: string * cterm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
@@ -229,16 +231,6 @@
 
 fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S;
 
-fun check_shyps ctxt sorts raw_th =
-  let
-    val th = Thm.strip_shyps raw_th;
-    val pending = Sorts.subtract sorts (Thm.extra_shyps th);
-  in
-    if null pending then th
-    else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
-      Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) pending))))
-  end;
-
 
 (* misc operations *)
 
@@ -274,22 +266,33 @@
 
 
 
-(** declared hyps **)
+(** declared hyps and sort hyps **)
 
 structure Hyps = Proof_Data
 (
-  type T = Termtab.set * bool;
-  fun init _ : T = (Termtab.empty, true);
+  type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T};
+  fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []};
 );
 
-fun declare_hyps raw_ct ctxt =
-  let val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct
-  in (Hyps.map o apfst) (Termtab.update (Thm.term_of ct, ())) ctxt end;
+fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} =>
+  let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps)
+  in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end);
+
+
+(* hyps *)
+
+fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) =>
+  let
+    val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct;
+    val hyps' = Termtab.update (Thm.term_of ct, ()) hyps;
+  in (checked_hyps, hyps', shyps) end);
 
 fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
 
-val unchecked_hyps = (Hyps.map o apsnd) (K false);
-fun restore_hyps ctxt = (Hyps.map o apsnd) (K (#2 (Hyps.get ctxt)));
+val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps));
+
+fun restore_hyps ctxt =
+  map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps));
 
 fun undeclared_hyps context th =
   Thm.hyps_of th
@@ -298,8 +301,8 @@
       Context.Theory _ => K false
     | Context.Proof ctxt =>
         (case Hyps.get ctxt of
-          (_, false) => K true
-        | (hyps, _) => Termtab.defined hyps));
+          {checked_hyps = false, ...} => K true
+        | {hyps, ...} => Termtab.defined hyps));
 
 fun check_hyps context th =
   (case undeclared_hyps context th of
@@ -309,6 +312,25 @@
         (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared))));
 
 
+(* shyps *)
+
+fun declare_term_sorts t =
+  map_hyps (fn (checked_hyps, hyps, shyps) =>
+    (checked_hyps, hyps, Sorts.insert_term t shyps));
+
+fun check_shyps ctxt raw_th =
+  let
+    val th = Thm.strip_shyps raw_th;
+    val pending = Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th);
+  in
+    if null pending then th
+    else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
+      Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) pending))))
+  end;
+
+val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get;
+
+
 
 (** basic derived rules **)
 

--- a/src/Pure/variable.ML	Fri Oct 23 16:09:06 2015 +0200
+++ b/src/Pure/variable.ML	Fri Oct 23 17:17:11 2015 +0200
@@ -9,7 +9,6 @@
   val names_of: Proof.context -> Name.context
   val binds_of: Proof.context -> (typ * term) Vartab.table
   val maxidx_of: Proof.context -> int
-  val sorts_of: Proof.context -> sort list
   val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
   val is_declared: Proof.context -> string -> bool
   val check_name: binding -> string
@@ -111,18 +110,17 @@
   binds: (typ * term) Vartab.table,     (*term bindings*)
   type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
   maxidx: int,                          (*maximum var index*)
-  sorts: sort Ord_List.T,               (*declared sort occurrences*)
   constraints:
     typ Vartab.table *                  (*type constraints*)
     sort Vartab.table};                 (*default sorts*)
 
-fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =
+fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =
   Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds,
-    type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
+    type_occs = type_occs, maxidx = maxidx, constraints = constraints};
 
 val empty_data =
   make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty,
-    Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty));
+    Symtab.empty, ~1, (Vartab.empty, Vartab.empty));
 
 structure Data = Proof_Data
 (
@@ -131,44 +129,40 @@
 );
 
 fun map_data f =
-  Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} =>
-    make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)));
+  Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, constraints} =>
+    make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints)));
 
 fun map_names f =
-  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
+    (f names, consts, bounds, fixes, binds, type_occs, maxidx, constraints));
 
 fun map_consts f =
-  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
+    (names, f consts, bounds, fixes, binds, type_occs, maxidx, constraints));
 
 fun map_bounds f =
-  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
+    (names, consts, f bounds, fixes, binds, type_occs, maxidx, constraints));
 
 fun map_fixes f =
-  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
+    (names, consts, bounds, f fixes, binds, type_occs, maxidx, constraints));
 
 fun map_binds f =
-  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
+    (names, consts, bounds, fixes, f binds, type_occs, maxidx, constraints));
 
 fun map_type_occs f =
-  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
+    (names, consts, bounds, fixes, binds, f type_occs, maxidx, constraints));
 
 fun map_maxidx f =
-  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints));
-
-fun map_sorts f =
-  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
+    (names, consts, bounds, fixes, binds, type_occs, f maxidx, constraints));
 
 fun map_constraints f =
-  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) =>
+    (names, consts, bounds, fixes, binds, type_occs, maxidx, f constraints));
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
 
@@ -178,7 +172,6 @@
 val binds_of = #binds o rep_data;
 val type_occs_of = #type_occs o rep_data;
 val maxidx_of = #maxidx o rep_data;
-val sorts_of = #sorts o rep_data;
 val constraints_of = #constraints o rep_data;
 
 val is_declared = Name.is_declared o names_of;
@@ -260,7 +253,7 @@
 fun declare_internal t =
   declare_names t #>
   declare_type_occs t #>
-  map_sorts (Sorts.insert_term t);
+  Thm.declare_term_sorts t;
 
 fun declare_term t =
   declare_internal t #>