diff -r d3053a55bfcb -r 3039922ffd8d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Oct 16 20:35:24 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 16 21:26:36 2012 +0200
@@ -709,12 +709,12 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
-    (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.also_cmd args)));
+    (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "finally"}
     "combine calculation and current facts, exhibit result"
-    (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.finally_cmd args)));
+    (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"