tuned;
authorwenzelm
Thu Mar 12 16:13:14 2009 +0100 (2009-03-12 ago)
changeset 30479fc58fb1f83ad
parent 30478 b0ce15e4633d
child 30480 f3421e8379ab
tuned;
src/Pure/assumption.ML
     1.1 --- a/src/Pure/assumption.ML	Thu Mar 12 15:56:32 2009 +0100
     1.2 +++ b/src/Pure/assumption.ML	Thu Mar 12 16:13:14 2009 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4  (** local context data **)
     1.5  
     1.6  datatype data = Data of
     1.7 - {assms: (export * cterm list) list,    (*assumes and views: A ==> _*)
     1.8 + {assms: (export * cterm list) list,    (*assumes: A ==> _*)
     1.9    prems: thm list};                     (*prems: A |- A*)
    1.10  
    1.11  fun make_data (assms, prems) = Data {assms = assms, prems = prems};
    1.12 @@ -110,11 +110,9 @@
    1.13  (* export *)
    1.14  
    1.15  fun export is_goal inner outer =
    1.16 -  let val asms = local_assumptions_of inner outer in
    1.17 -    MetaSimplifier.norm_hhf_protect
    1.18 -    #> fold_rev (fn (e, As) => #1 (e is_goal As)) asms
    1.19 -    #> MetaSimplifier.norm_hhf_protect
    1.20 -  end;
    1.21 +  MetaSimplifier.norm_hhf_protect #>
    1.22 +  fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
    1.23 +  MetaSimplifier.norm_hhf_protect;
    1.24  
    1.25  fun export_term inner outer =
    1.26    fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);