src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 27565 4bb03d4509e2
parent 27353 71c4dd53d4cb
child 27578 75945c883672
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jul 14 11:19:41 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jul 14 11:19:42 2008 +0200
     1.3 @@ -429,7 +429,7 @@
     1.4  fun isarcmd s = Isar.>>> (OuterSyntax.parse Position.none s);
     1.5  
     1.6  (* TODO:
     1.7 -    - apply a command given a transition function, e.g. IsarCmd.undo.
     1.8 +    - apply a command given a transition function;
     1.9      - fix position from path of currently open file [line numbers risk garbling though].
    1.10  *)
    1.11  
    1.12 @@ -549,7 +549,7 @@
    1.13          isarcmd ("undos_proof " ^ Int.toString times)
    1.14      end
    1.15  
    1.16 -fun redostep _ = isarcmd "redo"
    1.17 +fun redostep _ = sys_error "redo unavailable"
    1.18  
    1.19  fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
    1.20