src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 26622 e8e81ddb8919
parent 26613 725a3d9011d1
child 26706 4ea64590d28b
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 17:01:40 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 17:01:41 2008 +0200
     1.3 @@ -481,11 +481,7 @@
     1.4  
     1.5  (* Sending commands to Isar *)
     1.6  
     1.7 -fun isarcmd s =
     1.8 -    s |> OuterSyntax.scan |> OuterSyntax.read
     1.9 -      (*|> map (Toplevel.position Position.none o #3)*)
    1.10 -      |> map #3
    1.11 -      |> Isar.>>>;
    1.12 +fun isarcmd s = Isar.>>> (OuterSyntax.parse Position.none s);
    1.13  
    1.14  (* TODO:
    1.15      - apply a command given a transition function, e.g. IsarCmd.undo.