src/Pure/assumption.ML
changeset 30479 fc58fb1f83ad
parent 30471 178de3995e91
child 33519 e31a85f92ce9
--- a/src/Pure/assumption.ML	Thu Mar 12 15:56:32 2009 +0100
+++ b/src/Pure/assumption.ML	Thu Mar 12 16:13:14 2009 +0100
@@ -55,7 +55,7 @@
 (** local context data **)
 
 datatype data = Data of
- {assms: (export * cterm list) list,    (*assumes and views: A ==> _*)
+ {assms: (export * cterm list) list,    (*assumes: A ==> _*)
   prems: thm list};                     (*prems: A |- A*)
 
 fun make_data (assms, prems) = Data {assms = assms, prems = prems};
@@ -110,11 +110,9 @@
 (* export *)
 
 fun export is_goal inner outer =
-  let val asms = local_assumptions_of inner outer in
-    MetaSimplifier.norm_hhf_protect
-    #> fold_rev (fn (e, As) => #1 (e is_goal As)) asms
-    #> MetaSimplifier.norm_hhf_protect
-  end;
+  MetaSimplifier.norm_hhf_protect #>
+  fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
+  MetaSimplifier.norm_hhf_protect;
 
 fun export_term inner outer =
   fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);