src/Pure/Isar/isar_syn.ML
changeset 33390 5b499f36dd25
parent 33287 0f99569d23e1
child 33456 fbd47f9b9b12
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Nov 02 20:57:48 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 02 21:03:41 2009 +0100
     1.3 @@ -685,7 +685,7 @@
     1.4    OuterSyntax.command "proof" "backward proof"
     1.5      (K.tag_proof K.prf_block)
     1.6      (Scan.option Method.parse >> (fn m => Toplevel.print o
     1.7 -      Toplevel.actual_proof (ProofNode.applys (Proof.proof m)) o
     1.8 +      Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
     1.9        Toplevel.skip_proof (fn i => i + 1)));
    1.10  
    1.11  
    1.12 @@ -720,7 +720,7 @@
    1.13  val _ =
    1.14    OuterSyntax.command "back" "backtracking of proof command"
    1.15      (K.tag_proof K.prf_script)
    1.16 -    (Scan.succeed (Toplevel.print o Toplevel.actual_proof ProofNode.back o Toplevel.skip_proof I));
    1.17 +    (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
    1.18  
    1.19  
    1.20  (* nested commands *)