src/Pure/Proof/extraction.ML
changeset 24867 e5b55d7be9bb
parent 24712 64ed05609568
child 25389 3e58c7cb5a73
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -759,7 +759,7 @@
     1.4  
     1.5  val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
     1.6  
     1.7 -val realizersP =
     1.8 +val _ =
     1.9    OuterSyntax.command "realizers"
    1.10    "specify realizers for primitive axioms / theorems, together with correctness proof"
    1.11    K.thy_decl
    1.12 @@ -768,23 +768,21 @@
    1.13         (map (fn (((a, vs), s1), s2) =>
    1.14           (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy)));
    1.15  
    1.16 -val realizabilityP =
    1.17 +val _ =
    1.18    OuterSyntax.command "realizability"
    1.19    "add equations characterizing realizability" K.thy_decl
    1.20    (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns));
    1.21  
    1.22 -val typeofP =
    1.23 +val _ =
    1.24    OuterSyntax.command "extract_type"
    1.25    "add equations characterizing type of extracted program" K.thy_decl
    1.26    (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns));
    1.27  
    1.28 -val extractP =
    1.29 +val _ =
    1.30    OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
    1.31      (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
    1.32        (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy)));
    1.33  
    1.34 -val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
    1.35 -
    1.36  val etype_of = etype_of o add_syntax;
    1.37  
    1.38  end;