src/Pure/Isar/isar_syn.ML

--- a/src/Pure/Isar/isar_syn.ML	Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 16 15:14:12 2012 +0200
@@ -681,24 +681,25 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
-    (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
+    (Scan.option Parse.nat >> (fn n =>
+      (Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.defer n))));
 
 val _ =
   Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
-    (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
+    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.prefer n)));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
-    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
+    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement (unstructured)"
-    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
+    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
 
 val _ =
   Outer_Syntax.command @{command_spec "proof"} "backward proof"
     (Scan.option Method.parse >> (fn m => Toplevel.print o
-      Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
+      Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
       Toplevel.skip_proof (fn i => i + 1)));
 
 
@@ -709,12 +710,12 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
-    (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
+    (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.also_cmd args)));
 
 val _ =
   Outer_Syntax.command @{command_spec "finally"}
     "combine calculation and current facts, exhibit result"
-    (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
+    (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.finally_cmd args)));
 
 val _ =
   Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"