diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat May 15 23:16:32 2010 +0200
@@ -188,48 +188,44 @@
 
 (* additional outer syntax for Isar *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 fun prP () =
-  OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" K.diag
+  OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
       if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
       else (Toplevel.quiet := false; Toplevel.print_state true state))));
 
 fun undoP () = (*undo without output -- historical*)
-  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
+  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
 
 fun restartP () =
-  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
-    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
+  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
+    (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
 
 fun kill_proofP () =
-  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
+  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
     (Scan.succeed (Toplevel.no_timing o
       Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
 
 fun inform_file_processedP () =
-  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
-    (P.name >> (fn file =>
+  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
+    (Parse.name >> (fn file =>
       Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
 
 fun inform_file_retractedP () =
-  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
-    (P.name >> (Toplevel.no_timing oo
+  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
+    (Parse.name >> (Toplevel.no_timing oo
       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
 
 fun process_pgipP () =
-  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
-    (P.text >> (Toplevel.no_timing oo
+  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
+    (Parse.text >> (Toplevel.no_timing oo
       (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
 
 fun init_outer_syntax () = List.app (fn f => f ())
   [prP, undoP, restartP, kill_proofP, inform_file_processedP,
     inform_file_retractedP, process_pgipP];
 
-end;
-
 
 (* init *)