src/Pure/Proof/extraction.ML
changeset 36953 2af1ad9aa1a3
parent 36950 75b8f26f2f07
child 37233 b78f31ca4675
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat May 15 23:32:15 2010 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat May 15 23:40:00 2010 +0200
     1.3 @@ -753,7 +753,7 @@
     1.4  val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
     1.5  
     1.6  val _ =
     1.7 -  OuterSyntax.command "realizers"
     1.8 +  Outer_Syntax.command "realizers"
     1.9    "specify realizers for primitive axioms / theorems, together with correctness proof"
    1.10    Keyword.thy_decl
    1.11      (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
    1.12 @@ -761,17 +761,17 @@
    1.13         (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
    1.14  
    1.15  val _ =
    1.16 -  OuterSyntax.command "realizability"
    1.17 +  Outer_Syntax.command "realizability"
    1.18    "add equations characterizing realizability" Keyword.thy_decl
    1.19    (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
    1.20  
    1.21  val _ =
    1.22 -  OuterSyntax.command "extract_type"
    1.23 +  Outer_Syntax.command "extract_type"
    1.24    "add equations characterizing type of extracted program" Keyword.thy_decl
    1.25    (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
    1.26  
    1.27  val _ =
    1.28 -  OuterSyntax.command "extract" "extract terms from proofs" Keyword.thy_decl
    1.29 +  Outer_Syntax.command "extract" "extract terms from proofs" Keyword.thy_decl
    1.30      (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
    1.31        extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
    1.32