src/Pure/Proof/extraction.ML
changeset 39557 fe5722fce758
parent 39288 f1ae2493d93f
child 40132 7ee65dbffa31
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -783,11 +783,11 @@
     1.4               val (def_thms, thy') = if t = nullt then ([], thy) else
     1.5                 thy
     1.6                 |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
     1.7 -               |> PureThy.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"),
     1.8 +               |> Global_Theory.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"),
     1.9                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
    1.10             in
    1.11               thy'
    1.12 -             |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
    1.13 +             |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
    1.14                    Thm.varifyT_global (funpow (length (vars_of corr_prop))
    1.15                      (Thm.forall_elim_var 0) (Thm.forall_intr_frees
    1.16                        (ProofChecker.thm_of_proof thy'
    1.17 @@ -815,7 +815,7 @@
    1.18    Keyword.thy_decl
    1.19      (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
    1.20       (fn xs => Toplevel.theory (fn thy => add_realizers
    1.21 -       (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
    1.22 +       (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
    1.23  
    1.24  val _ =
    1.25    Outer_Syntax.command "realizability"
    1.26 @@ -830,7 +830,7 @@
    1.27  val _ =
    1.28    Outer_Syntax.command "extract" "extract terms from proofs" Keyword.thy_decl
    1.29      (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
    1.30 -      extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
    1.31 +      extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
    1.32  
    1.33  val etype_of = etype_of o add_syntax;
    1.34