# HG changeset patch
# User wenzelm
# Date 1330807935 -3600
# Node ID 8575cc482dfbf118b939649f13e11729f2392da1
# Parent  6287653e63ece84221ccd4f64e9fad7283fb771b
tuned;

diff -r 6287653e63ec -r 8575cc482dfb src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Mar 03 21:43:59 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Mar 03 21:52:15 2012 +0100
@@ -415,7 +415,7 @@
     |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
     |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
         error "Illegal schematic goal statement")
-    |> Library.apply (map (fn (f, _) => f int) (rev (Theorem_Hook.get (Context.Proof goal_ctxt))))
+    |> fold_rev (fn (f, _) => f int) (Theorem_Hook.get (Context.Proof goal_ctxt))
   end;
 
 in
diff -r 6287653e63ec -r 8575cc482dfb src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Mar 03 21:43:59 2012 +0100
+++ b/src/Pure/simplifier.ML	Sat Mar 03 21:52:15 2012 +0100
@@ -315,7 +315,7 @@
   (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) =>
     Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt))))
   >> (fn atts => Thm.declaration_attribute (fn th =>
-        Library.apply (map (fn att => Thm.attribute_declaration (Morphism.form att) th) atts)));
+        fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts));
 
 end;