src/Pure/ProofGeneral/proof_general_pgip.ML

 
 
 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
 
 fun lexicalstructure_keywords () =
-    let val keywords = OuterKeyword.dest_keywords ()
-        val commands = OuterKeyword.dest_commands ()
+    let val keywords = Keyword.dest_keywords ()
+        val commands = Keyword.dest_commands ()
         fun keyword_elt kind keyword =
             XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
         in
             (* Also, note we don't call init_outer_syntax here to add interface commands,
             but they should never appear in scripts anyway so it shouldn't matter *)

 
 
 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
 
 fun init_outer_syntax () =
-  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
-    (OuterParse.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 () => process_pgip_plain txt))));
 
 
 (* init *)