# HG changeset patch
# User wenzelm
# Date 1207839701 -7200
# Node ID e8e81ddb89195bd2e8a8550d739d734abeb72673
# Parent  78b3ad7af5d5e6ae5cad2b606e9a989ddbe90b15
simplified isarcmd;

diff -r 78b3ad7af5d5 -r e8e81ddb8919 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 17:01:40 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 17:01:41 2008 +0200
@@ -481,11 +481,7 @@
 
 (* Sending commands to Isar *)
 
-fun isarcmd s =
-    s |> OuterSyntax.scan |> OuterSyntax.read
-      (*|> map (Toplevel.position Position.none o #3)*)
-      |> map #3
-      |> Isar.>>>;
+fun isarcmd s = Isar.>>> (OuterSyntax.parse Position.none s);
 
 (* TODO:
     - apply a command given a transition function, e.g. IsarCmd.undo.