src/Pure/Proof/extraction.ML
changeset 46961 5c6955f487e5
parent 46909 3c73a121a387
child 48646 91281e9472d8
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -820,25 +820,24 @@
     1.4  val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.command "realizers"
     1.8 -  "specify realizers for primitive axioms / theorems, together with correctness proof"
     1.9 -  Keyword.thy_decl
    1.10 +  Outer_Syntax.command ("realizers", Keyword.thy_decl)
    1.11 +    "specify realizers for primitive axioms / theorems, together with correctness proof"
    1.12      (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
    1.13       (fn xs => Toplevel.theory (fn thy => add_realizers
    1.14         (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
    1.15  
    1.16  val _ =
    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 +  Outer_Syntax.command ("realizability", Keyword.thy_decl)
    1.21 +    "add equations characterizing realizability"
    1.22 +    (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
    1.23  
    1.24  val _ =
    1.25 -  Outer_Syntax.command "extract_type"
    1.26 -  "add equations characterizing type of extracted program" Keyword.thy_decl
    1.27 -  (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
    1.28 +  Outer_Syntax.command ("extract_type", Keyword.thy_decl)
    1.29 +    "add equations characterizing type of extracted program"
    1.30 +    (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
    1.31  
    1.32  val _ =
    1.33 -  Outer_Syntax.command "extract" "extract terms from proofs" Keyword.thy_decl
    1.34 +  Outer_Syntax.command ("extract", Keyword.thy_decl) "extract terms from proofs"
    1.35      (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
    1.36        extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
    1.37