src/Pure/Isar/isar_syn.ML
changeset 49865 eeaf1ec7eac2
parent 49863 b5fb6e7f8d81
child 49868 3039922ffd8d
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Oct 16 16:50:03 2012 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 16 17:47:23 2012 +0200
     1.3 @@ -681,12 +681,11 @@
     1.4  
     1.5  val _ =
     1.6    Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
     1.7 -    (Scan.option Parse.nat >> (fn n =>
     1.8 -      (Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.defer n))));
     1.9 +    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (Proof.defer n)));
    1.10  
    1.11  val _ =
    1.12    Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
    1.13 -    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.prefer n)));
    1.14 +    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proof (Proof.prefer n)));
    1.15  
    1.16  val _ =
    1.17    Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"