more elementary management of declared hyps, below structure Assumption;
Goal.prove: insist in declared hyps;
Simplifier: declare hyps via Thm.assume_hyps;
more accurate tool context in some boundary cases;

--- a/src/HOL/Tools/Function/mutual.ML	Fri Jan 10 17:44:41 2014 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Jan 10 21:37:28 2014 +0100
@@ -187,8 +187,7 @@
       | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
       | _ => raise General.Fail "Too many conditions"
 
-    val (_, simp_ctxt) = ctxt
-      |> Assumption.add_assumes (#hyps (Thm.crep_thm simp))
+    val simp_ctxt = fold Thm.declare_hyps (#hyps (Thm.crep_thm simp)) ctxt
   in
     Goal.prove simp_ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Jan 10 17:44:41 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Jan 10 21:37:28 2014 +0100
@@ -425,16 +425,17 @@
         val (prems0, concl) = th |> prop_of |> Logic.strip_horn
         val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped
         val goal = Logic.list_implies (prems, concl)
+        val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt
         val tac =
           cut_tac th 1
-          THEN rewrite_goals_tac ctxt @{thms not_not [THEN eq_reflection]}
+          THEN rewrite_goals_tac ctxt' @{thms not_not [THEN eq_reflection]}
           THEN ALLGOALS assume_tac
       in
         if length prems = length prems0 then
           raise METIS_RECONSTRUCT ("resynchronize", "Out of sync")
         else
-          Goal.prove ctxt [] [] goal (K tac)
-          |> resynchronize ctxt fol_th
+          Goal.prove ctxt' [] [] goal (K tac)
+          |> resynchronize ctxt' fol_th
       end
   end
 
@@ -722,8 +723,9 @@
         THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
       fun rotation_of_subgoal i =
         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
+      val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt
     in
-      Goal.prove ctxt [] [] @{prop False}
+      Goal.prove ctxt' [] [] @{prop False}
           (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
                                   o fst) ax_counts)
                       THEN rename_tac outer_param_names 1
@@ -736,9 +738,9 @@
                        THEN PRIMITIVE (unify_first_prem_with_concl thy i)
                        THEN assume_tac i
                        THEN flexflex_tac)))
-      handle ERROR _ =>
-             error ("Cannot replay Metis proof in Isabelle:\n\
-                    \Error when discharging Skolem assumptions.")
+      handle ERROR msg =>
+        cat_error msg
+          "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions."
     end
 
 end;

--- a/src/HOL/ex/Meson_Test.thy	Fri Jan 10 17:44:41 2014 +0100
+++ b/src/HOL/ex/Meson_Test.thy	Fri Jan 10 21:37:28 2014 +0100
@@ -37,7 +37,7 @@
     val horns25 = Meson.make_horns clauses25;     (*16 Horn clauses*)
     val go25 :: _ = Meson.gocls clauses25;
 
-    val (_, ctxt') = Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt;
+    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt;
     Goal.prove ctxt' [] [] @{prop False} (fn _ =>
       rtac go25 1 THEN
       Meson.depth_prolog_tac horns25);
@@ -63,7 +63,7 @@
     val _ = @{assert} (length horns26 = 24);
     val go26 :: _ = Meson.gocls clauses26;
 
-    val (_, ctxt') = Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt;
+    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt;
     Goal.prove ctxt' [] [] @{prop False} (fn _ =>
       rtac go26 1 THEN
       Meson.depth_prolog_tac horns26);  (*7 ms*)
@@ -90,7 +90,7 @@
     val _ = @{assert} (length horns43 = 16);
     val go43 :: _ = Meson.gocls clauses43;
 
-    val (_, ctxt') = Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt;
+    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt;
     Goal.prove ctxt' [] [] @{prop False} (fn _ =>
       rtac go43 1 THEN
       Meson.best_prolog_tac Meson.size_of_subgoals horns43);   (*7ms*)

--- a/src/Pure/Isar/proof.ML	Fri Jan 10 17:44:41 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Jan 10 21:37:28 2014 +0100
@@ -492,7 +492,7 @@
         handle THM _ => lost_structure ())
       |> Drule.flexflex_unique
       |> Thm.check_shyps (Variable.sorts_of ctxt)
-      |> Assumption.check_hyps ctxt;
+      |> Thm.check_hyps ctxt;
 
     val goal_propss = filter_out null propss;
     val results =

--- a/src/Pure/assumption.ML	Fri Jan 10 17:44:41 2014 +0100
+++ b/src/Pure/assumption.ML	Fri Jan 10 21:37:28 2014 +0100
@@ -10,9 +10,9 @@
   val assume_export: export
   val presume_export: export
   val assume: Proof.context -> cterm -> thm
+  val assume_hyps: cterm -> Proof.context -> thm * Proof.context
   val all_assms_of: Proof.context -> cterm list
   val all_prems_of: Proof.context -> thm list
-  val check_hyps: Proof.context -> thm -> thm
   val local_assms_of: Proof.context -> Proof.context -> cterm list
   val local_prems_of: Proof.context -> Proof.context -> thm list
   val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
@@ -48,8 +48,13 @@
 *)
 fun presume_export _ = assume_export false;
 
+
 fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume;
 
+fun assume_hyps ct ctxt =
+  let val (th, ctxt') = Thm.assume_hyps ct ctxt
+  in (Raw_Simplifier.norm_hhf ctxt' th, ctxt') end;
+
 
 
 (** local context data **)
@@ -76,13 +81,6 @@
 val all_assms_of = maps #2 o all_assumptions_of;
 val all_prems_of = #prems o rep_data;
 
-fun check_hyps ctxt th =
-  let
-    val extra_hyps = subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
-    val _ = null extra_hyps orelse
-      error ("Additional hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) extra_hyps));
-  in th end;
-
 
 (* local assumptions *)
 
@@ -98,8 +96,8 @@
 (* add assumptions *)
 
 fun add_assms export new_asms ctxt =
-  let val new_prems = map (assume ctxt) new_asms in
-    ctxt
+  let val (new_prems, ctxt') = fold_map assume_hyps new_asms ctxt in
+    ctxt'
     |> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems))
     |> pair new_prems
   end;

--- a/src/Pure/goal.ML	Fri Jan 10 17:44:41 2014 +0100
+++ b/src/Pure/goal.ML	Fri Jan 10 21:37:28 2014 +0100
@@ -221,7 +221,7 @@
               (finish ctxt' st
                 |> Drule.flexflex_unique
                 |> Thm.check_shyps sorts
-                (* |> Assumption.check_hyps ctxt' FIXME *))
+                |> Thm.check_hyps ctxt')
               handle THM (msg, _, _) => err msg | ERROR msg => err msg;
           in
             if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res

--- a/src/Pure/more_thm.ML	Fri Jan 10 17:44:41 2014 +0100
+++ b/src/Pure/more_thm.ML	Fri Jan 10 21:37:28 2014 +0100
@@ -52,6 +52,9 @@
   val full_rules: thm Item_Net.T
   val intro_rules: thm Item_Net.T
   val elim_rules: thm Item_Net.T
+  val declare_hyps: cterm -> Proof.context -> Proof.context
+  val assume_hyps: cterm -> Proof.context -> thm * Proof.context
+  val check_hyps: Proof.context -> thm -> thm
   val elim_implies: thm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
@@ -259,6 +262,30 @@
 
 
 
+(** declared hyps **)
+
+structure Hyps = Proof_Data
+(
+  type T = Termtab.set;
+  fun init _ : T = Termtab.empty;
+);
+
+fun declare_hyps ct ctxt =
+  if Theory.subthy (theory_of_cterm ct, Proof_Context.theory_of ctxt) then
+    Hyps.map (Termtab.update (term_of ct, ())) ctxt
+  else raise CTERM ("assume_hyps: bad background theory", [ct]);
+
+fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
+
+fun check_hyps ctxt th =
+  let
+    val undeclared = filter_out (Termtab.defined (Hyps.get ctxt)) (Thm.hyps_of th);
+    val _ = null undeclared orelse
+      error ("Undeclared hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) undeclared));
+  in th end;
+
+
+
 (** basic derived rules **)
 
 (*Elimination of implication

--- a/src/Pure/raw_simplifier.ML	Fri Jan 10 17:44:41 2014 +0100
+++ b/src/Pure/raw_simplifier.ML	Fri Jan 10 21:37:28 2014 +0100
@@ -1190,14 +1190,14 @@
       if mutsimp then mut_impc0 [] ct [] [] ctxt
       else nonmut_impc ct ctxt
 
-    and rules_of_prem ctxt prem =
+    and rules_of_prem prem ctxt =
       if maxidx_of_term (term_of prem) <> ~1
       then (trace_cterm ctxt true
         (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
-        prem; ([], NONE))
+        prem; (([], NONE), ctxt))
       else
-        let val asm = Thm.assume prem
-        in (extract_safe_rrules ctxt asm, SOME asm) end
+        let val (asm, ctxt') = Thm.assume_hyps prem ctxt
+        in ((extract_safe_rrules ctxt' asm, SOME asm), ctxt') end
 
     and add_rrules (rrss, asms) ctxt =
       (fold o fold) insert_rrule rrss ctxt |> add_prems (map_filter I asms)
@@ -1242,10 +1242,10 @@
     and mut_impc0 prems concl rrss asms ctxt =
       let
         val prems' = strip_imp_prems concl;
-        val (rrss', asms') = split_list (map (rules_of_prem ctxt) prems');
+        val ((rrss', asms'), ctxt') = fold_map rules_of_prem prems' ctxt |>> split_list;
       in
         mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
-          (asms @ asms') [] [] [] [] ctxt ~1 ~1
+          (asms @ asms') [] [] [] [] ctxt' ~1 ~1
       end
 
     and mut_impc [] concl [] [] prems' rrss' asms' eqns ctxt changed k =
@@ -1270,7 +1270,7 @@
               val tprems = map term_of prems;
               val i = 1 + fold Integer.max (map (fn p =>
                 find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
-              val (rrs', asm') = rules_of_prem ctxt prem';
+              val ((rrs', asm'), ctxt') = rules_of_prem prem' ctxt;
             in
               mut_impc prems concl rrss asms (prem' :: prems')
                 (rrs' :: rrss') (asm' :: asms')
@@ -1278,7 +1278,7 @@
                   (take i prems)
                   (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
                     (drop i prems, concl))))) :: eqns)
-                ctxt (length prems') ~1
+                ctxt' (length prems') ~1
             end)
 
     (*legacy code -- only for backwards compatibility*)
@@ -1289,7 +1289,9 @@
         val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
         val ctxt1 =
           if not useprem then ctxt
-          else add_rrules (apsnd single (apfst single (rules_of_prem ctxt prem1))) ctxt
+          else
+            let val ((rrs, asm), ctxt') = rules_of_prem prem1 ctxt
+            in add_rrules ([rrs], [asm]) ctxt' end;
       in
         (case botc skel0 ctxt1 conc of
           NONE =>