assms_of: cterm;
authorwenzelm
Wed Nov 29 04:11:10 2006 +0100 (2006-11-29 ago)
changeset 215773ff126ca39b4
parent 21576 8c11b1ce2f05
child 21578 a89f786b301a
assms_of: cterm;
src/Pure/assumption.ML
     1.1 --- a/src/Pure/assumption.ML	Wed Nov 29 04:11:09 2006 +0100
     1.2 +++ b/src/Pure/assumption.ML	Wed Nov 29 04:11:10 2006 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4    val assume_export: export
     1.5    val presume_export: export
     1.6    val assume: cterm -> thm
     1.7 -  val assms_of: Proof.context -> term list
     1.8 +  val assms_of: Proof.context -> cterm list
     1.9    val prems_of: Proof.context -> thm list
    1.10    val extra_hyps: Proof.context -> thm -> term list
    1.11    val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
    1.12 @@ -73,10 +73,10 @@
    1.13  fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
    1.14  
    1.15  val assumptions_of = #assms o rep_data;
    1.16 -val assms_of = map Thm.term_of o maps #2 o assumptions_of;
    1.17 +val assms_of = maps #2 o assumptions_of;
    1.18  val prems_of = #prems o rep_data;
    1.19  
    1.20 -fun extra_hyps ctxt th = subtract (op aconv) (assms_of ctxt) (Thm.hyps_of th);
    1.21 +fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th);
    1.22  
    1.23  
    1.24  (* add assumptions *)