# HG changeset patch
# User wenzelm
# Date 1236870794 -3600
# Node ID fc58fb1f83ad35be82237c2b44142f7a8ddd2467
# Parent  b0ce15e4633d4131b1a9147ac7e4adeb9f7c970b
tuned;

diff -r b0ce15e4633d -r fc58fb1f83ad src/Pure/assumption.ML
--- 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);