author | wenzelm |
Thu, 10 Apr 2008 17:01:41 +0200 | |
changeset 26622 | e8e81ddb8919 |
parent 26621 | 78b3ad7af5d5 |
child 26623 | 81547c8d51f8 |
--- 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.