--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Aug 02 11:32:23 2012 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Aug 02 12:36:54 2012 +0200
@@ -1032,7 +1032,8 @@
(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
val _ =
- Outer_Syntax.improper_command ("ProofGeneral.process_pgip", Keyword.control) "(internal)"
+ Outer_Syntax.improper_command
+ (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)"
(Parse.text >> (Toplevel.no_timing oo
(fn txt => Toplevel.imperative (fn () =>
if print_mode_active proof_general_emacsN