simplified isarcmd;
authorwenzelm
Thu, 10 Apr 2008 17:01:41 +0200
changeset 26622e8e81ddb8919
parent 26621 78b3ad7af5d5
child 26623 81547c8d51f8
simplified isarcmd;
src/Pure/ProofGeneral/proof_general_pgip.ML
     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.