--- 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
--- 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;