src/Pure/assumption.ML
changeset 54567 cfe53047dc16
parent 47236 973ab740a25d
child 54740 91f54d386680
     1.1 --- a/src/Pure/assumption.ML	Sat Nov 23 17:07:36 2013 +0100
     1.2 +++ b/src/Pure/assumption.ML	Sat Nov 23 17:15:44 2013 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    val assume: cterm -> thm
     1.5    val all_assms_of: Proof.context -> cterm list
     1.6    val all_prems_of: Proof.context -> thm list
     1.7 -  val extra_hyps: Proof.context -> thm -> term list
     1.8 +  val check_hyps: Proof.context -> thm -> thm
     1.9    val local_assms_of: Proof.context -> Proof.context -> cterm list
    1.10    val local_prems_of: Proof.context -> Proof.context -> thm list
    1.11    val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
    1.12 @@ -76,8 +76,12 @@
    1.13  val all_assms_of = maps #2 o all_assumptions_of;
    1.14  val all_prems_of = #prems o rep_data;
    1.15  
    1.16 -fun extra_hyps ctxt th =
    1.17 -  subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
    1.18 +fun check_hyps ctxt th =
    1.19 +  let
    1.20 +    val extra_hyps = subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
    1.21 +    val _ = null extra_hyps orelse
    1.22 +      error ("Additional hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) extra_hyps));
    1.23 +  in th end;
    1.24  
    1.25  
    1.26  (* local assumptions *)