--- 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;