src/Pure/Isar/isar_syn.ML

--- a/src/Pure/Isar/isar_syn.ML	Tue Oct 16 16:50:03 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 16 17:47:23 2012 +0200
@@ -681,12 +681,11 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
-    (Scan.option Parse.nat >> (fn n =>
-      (Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.defer n))));
+    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (Proof.defer n)));
 
 val _ =
   Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
-    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.prefer n)));
+    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proof (Proof.prefer n)));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"