1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -1125,21 +1125,13 @@
     1.4  end
     1.5  
     1.6  
     1.7 -local
     1.8  (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
     1.9  
    1.10 -val process_pgipP =
    1.11 +fun init_outer_syntax () =
    1.12    OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
    1.13      (OuterParse.text >> (Toplevel.no_timing oo
    1.14        (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
    1.15  
    1.16 -in
    1.17 -
    1.18 - fun init_outer_syntax () = OuterSyntax.add_parsers [process_pgipP];
    1.19 -
    1.20 -end
    1.21 -
    1.22 -
    1.23  
    1.24  (* init *)
    1.25