diff -r 2c57fc1f7a8c -r da70ab8531f4 src/Pure/assumption.ML
--- 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;