src/Pure/Proof/extraction.ML
changeset 36950 75b8f26f2f07
parent 36744 6e1f3d609a68
child 36953 2af1ad9aa1a3
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat May 15 22:24:25 2010 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat May 15 23:16:32 2010 +0200
     1.3 @@ -750,31 +750,29 @@
     1.4  
     1.5  (**** interface ****)
     1.6  
     1.7 -structure P = OuterParse and K = OuterKeyword;
     1.8 -
     1.9 -val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
    1.10 +val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
    1.11  
    1.12  val _ =
    1.13    OuterSyntax.command "realizers"
    1.14    "specify realizers for primitive axioms / theorems, together with correctness proof"
    1.15 -  K.thy_decl
    1.16 -    (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
    1.17 +  Keyword.thy_decl
    1.18 +    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
    1.19       (fn xs => Toplevel.theory (fn thy => add_realizers
    1.20         (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
    1.21  
    1.22  val _ =
    1.23    OuterSyntax.command "realizability"
    1.24 -  "add equations characterizing realizability" K.thy_decl
    1.25 -  (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns));
    1.26 +  "add equations characterizing realizability" Keyword.thy_decl
    1.27 +  (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
    1.28  
    1.29  val _ =
    1.30    OuterSyntax.command "extract_type"
    1.31 -  "add equations characterizing type of extracted program" K.thy_decl
    1.32 -  (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns));
    1.33 +  "add equations characterizing type of extracted program" Keyword.thy_decl
    1.34 +  (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
    1.35  
    1.36  val _ =
    1.37 -  OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
    1.38 -    (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
    1.39 +  OuterSyntax.command "extract" "extract terms from proofs" Keyword.thy_decl
    1.40 +    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
    1.41        extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
    1.42  
    1.43  val etype_of = etype_of o add_syntax;