renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
authorwenzelm
Mon Sep 20 16:05:25 2010 +0200 (2010-09-20)
changeset 39557fe5722fce758
parent 39556 32a00ff29d1a
child 39563 0fa447d9aa2e
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
NEWS
src/CTT/CTT.thy
src/Cube/Cube.thy
src/FOL/IFOL.thy
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/FOLP/IFOLP.thy
src/HOL/Import/hol4rews.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Import/shuffler.ML
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Mutabelle/Mutabelle.thy
src/HOL/Mutabelle/mutabelle.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/String.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/record.ML
src/HOLCF/Tools/Domain/domain_constructors.ML
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/Tools/fixrec.ML
src/HOLCF/Tools/pcpodef.ML
src/HOLCF/Tools/repdef.ML
src/HOLCF/ex/Pattern_Match.thy
src/Pure/IsaMakefile
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/class.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/named_target.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/specification.ML
src/Pure/ML/ml_context.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/proofchecker.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/ROOT.ML
src/Pure/Thy/thm_deps.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/named_thms.ML
src/Pure/assumption.ML
src/Pure/axclass.ML
src/Pure/drule.ML
src/Pure/global_theory.ML
src/Pure/pure_thy.ML
src/Sequents/Sequents.thy
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/NEWS	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/NEWS	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -244,6 +244,10 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Renamed structure PureThy to Pure_Thy and moved most of its
     1.8 +operations to structure Global_Theory, to emphasize that this is
     1.9 +rarely-used global-only stuff.
    1.10 +
    1.11  * Discontinued Output.debug.  Minor INCOMPATIBILITY, use plain writeln
    1.12  instead (or tracing for high-volume output).
    1.13  
     2.1 --- a/src/CTT/CTT.thy	Mon Sep 20 15:29:53 2010 +0200
     2.2 +++ b/src/CTT/CTT.thy	Mon Sep 20 16:05:25 2010 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  uses "~~/src/Provers/typedsimp.ML" ("rew.ML")
     2.5  begin
     2.6  
     2.7 -setup PureThy.old_appl_syntax_setup
     2.8 +setup Pure_Thy.old_appl_syntax_setup
     2.9  
    2.10  typedecl i
    2.11  typedecl t
     3.1 --- a/src/Cube/Cube.thy	Mon Sep 20 15:29:53 2010 +0200
     3.2 +++ b/src/Cube/Cube.thy	Mon Sep 20 16:05:25 2010 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  imports Pure
     3.5  begin
     3.6  
     3.7 -setup PureThy.old_appl_syntax_setup
     3.8 +setup Pure_Thy.old_appl_syntax_setup
     3.9  
    3.10  typedecl "term"
    3.11  typedecl "context"
     4.1 --- a/src/FOL/IFOL.thy	Mon Sep 20 15:29:53 2010 +0200
     4.2 +++ b/src/FOL/IFOL.thy	Mon Sep 20 16:05:25 2010 +0200
     4.3 @@ -26,7 +26,7 @@
     4.4  
     4.5  subsection {* Syntax and axiomatic basis *}
     4.6  
     4.7 -setup PureThy.old_appl_syntax_setup
     4.8 +setup Pure_Thy.old_appl_syntax_setup
     4.9  
    4.10  classes "term"
    4.11  default_sort "term"
     5.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Sep 20 15:29:53 2010 +0200
     5.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Sep 20 16:05:25 2010 +0200
     5.3 @@ -442,7 +442,7 @@
     5.4  interpretation int2?: semi "op +"
     5.5    by unfold_locales  (* subsumed, thm int2.assoc not generated *)
     5.6  
     5.7 -ML {* (PureThy.get_thms @{theory} "int2.assoc";
     5.8 +ML {* (Global_Theory.get_thms @{theory} "int2.assoc";
     5.9      error "thm int2.assoc was generated")
    5.10    handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
    5.11  
     6.1 --- a/src/FOLP/IFOLP.thy	Mon Sep 20 15:29:53 2010 +0200
     6.2 +++ b/src/FOLP/IFOLP.thy	Mon Sep 20 16:05:25 2010 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4  uses ("hypsubst.ML") ("intprover.ML")
     6.5  begin
     6.6  
     6.7 -setup PureThy.old_appl_syntax_setup
     6.8 +setup Pure_Thy.old_appl_syntax_setup
     6.9  
    6.10  classes "term"
    6.11  default_sort "term"
     7.1 --- a/src/HOL/Import/hol4rews.ML	Mon Sep 20 15:29:53 2010 +0200
     7.2 +++ b/src/HOL/Import/hol4rews.ML	Mon Sep 20 16:05:25 2010 +0200
     7.3 @@ -370,7 +370,7 @@
     7.4          val thm2 = Drule.export_without_context thm1;
     7.5        in
     7.6          thy
     7.7 -        |> PureThy.store_thm (Binding.name bthm, thm2)
     7.8 +        |> Global_Theory.store_thm (Binding.name bthm, thm2)
     7.9          |> snd
    7.10          |> add_hol4_theorem bthy bthm hth
    7.11        end;
     8.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Sep 20 15:29:53 2010 +0200
     8.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Sep 20 16:05:25 2010 +0200
     8.3 @@ -1261,10 +1261,10 @@
     8.4          case get_hol4_mapping thyname thmname thy of
     8.5              SOME (SOME thmname) =>
     8.6              let
     8.7 -                val th1 = (SOME (PureThy.get_thm thy thmname)
     8.8 +                val th1 = (SOME (Global_Theory.get_thm thy thmname)
     8.9                             handle ERROR _ =>
    8.10                                    (case split_name thmname of
    8.11 -                                       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
    8.12 +                                       SOME (listname,idx) => (SOME (List.nth(Global_Theory.get_thms thy listname,idx-1))
    8.13                                                                 handle _ => NONE)  (* FIXME avoid handle _ *)
    8.14                                       | NONE => NONE))
    8.15              in
    8.16 @@ -1922,7 +1922,7 @@
    8.17                       | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)];
    8.18                                Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy)
    8.19          val eq = mk_defeq constname rhs' thy1
    8.20 -        val (thms, thy2) = PureThy.add_defs false [((Binding.name thmname,eq),[])] thy1
    8.21 +        val (thms, thy2) = Global_Theory.add_defs false [((Binding.name thmname,eq),[])] thy1
    8.22          val _ = ImportRecorder.add_defs thmname eq
    8.23          val def_thm = hd thms
    8.24          val thm' = def_thm RS meta_eq_to_obj_eq_thm
    8.25 @@ -2144,7 +2144,7 @@
    8.26  fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
    8.27      case HOL4DefThy.get thy of
    8.28          Replaying _ => (thy,
    8.29 -          HOLThm([], PureThy.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
    8.30 +          HOLThm([], Global_Theory.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
    8.31        | _ =>
    8.32          let
    8.33              val _ = message "TYPE_INTRO:"
     9.1 --- a/src/HOL/Import/replay.ML	Mon Sep 20 15:29:53 2010 +0200
     9.2 +++ b/src/HOL/Import/replay.ML	Mon Sep 20 16:05:25 2010 +0200
     9.3 @@ -339,7 +339,7 @@
     9.4            | delta (Hol_move (fullname, moved_thmname)) thy = 
     9.5              add_hol4_move fullname moved_thmname thy
     9.6            | delta (Defs (thmname, eq)) thy =
     9.7 -            snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
     9.8 +            snd (Global_Theory.add_defs false [((Binding.name thmname, eq), [])] thy)
     9.9            | delta (Hol_theorem (thyname, thmname, th)) thy =
    9.10              add_hol4_theorem thyname thmname ([], th_of thy th) thy
    9.11            | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
    10.1 --- a/src/HOL/Import/shuffler.ML	Mon Sep 20 15:29:53 2010 +0200
    10.2 +++ b/src/HOL/Import/shuffler.ML	Mon Sep 20 16:05:25 2010 +0200
    10.3 @@ -623,7 +623,7 @@
    10.4          val shuffles = ShuffleData.get thy
    10.5          val ignored = collect_ignored shuffles []
    10.6          val all_thms =
    10.7 -          map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
    10.8 +          map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (Global_Theory.facts_of thy)))
    10.9      in
   10.10          filter (match_consts ignored t) all_thms
   10.11      end
    11.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon Sep 20 15:29:53 2010 +0200
    11.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon Sep 20 16:05:25 2010 +0200
    11.3 @@ -183,7 +183,7 @@
    11.4  
    11.5  fun theorems_in_proof_term thm =
    11.6    let
    11.7 -    val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
    11.8 +    val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm)
    11.9      fun collect (s, _, _) = if s <> "" then insert (op =) s else I
   11.10      fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
   11.11      fun resolve_thms names = map_filter (member_of names) all_thms
    12.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Mon Sep 20 15:29:53 2010 +0200
    12.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Mon Sep 20 16:05:25 2010 +0200
    12.3 @@ -75,12 +75,12 @@
    12.4  fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
    12.5     Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
    12.6     is_executable thy th)
    12.7 - (PureThy.all_thms_of thy);
    12.8 + (Global_Theory.all_thms_of thy);
    12.9  
   12.10  fun find_thm thy = find_first (fn (_, th) => not (Thm.is_internal th) andalso
   12.11     Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
   12.12     is_executable thy th)
   12.13 - (PureThy.all_thms_of thy);
   12.14 + (Global_Theory.all_thms_of thy);
   12.15  *}
   12.16  
   12.17  ML {*
    13.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Mon Sep 20 15:29:53 2010 +0200
    13.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Mon Sep 20 16:05:25 2010 +0200
    13.3 @@ -59,7 +59,7 @@
    13.4  
    13.5  fun all_unconcealed_thms_of thy =
    13.6    let
    13.7 -    val facts = PureThy.facts_of thy
    13.8 +    val facts = Global_Theory.facts_of thy
    13.9    in
   13.10      Facts.fold_static
   13.11        (fn (s, ths) =>
    14.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon Sep 20 15:29:53 2010 +0200
    14.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Sep 20 16:05:25 2010 +0200
    14.3 @@ -88,8 +88,8 @@
    14.4    let val T = fastype_of x
    14.5    in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
    14.6  
    14.7 -fun add_thms_string args = PureThy.add_thms ((map o apfst o apfst) Binding.name args);
    14.8 -fun add_thmss_string args = PureThy.add_thmss ((map o apfst o apfst) Binding.name args);
    14.9 +fun add_thms_string args = Global_Theory.add_thms ((map o apfst o apfst) Binding.name args);
   14.10 +fun add_thmss_string args = Global_Theory.add_thmss ((map o apfst o apfst) Binding.name args);
   14.11  
   14.12  (* this function sets up all matters related to atom-  *)
   14.13  (* kinds; the user specifies a list of atom-kind names *)
   14.14 @@ -189,7 +189,7 @@
   14.15          val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
   14.16        in
   14.17          thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)] 
   14.18 -            |> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])]
   14.19 +            |> Global_Theory.add_defs_unchecked true [((Binding.name name, def2),[])]
   14.20              |> snd
   14.21              |> OldPrimrec.add_primrec_unchecked_i "" [(("", def1),[])]
   14.22        end) ak_names_types thy1;
   14.23 @@ -244,7 +244,7 @@
   14.24            val def = Logic.mk_equals
   14.25                      (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
   14.26          in
   14.27 -          PureThy.add_defs_unchecked true [((Binding.name name, def),[])] thy'
   14.28 +          Global_Theory.add_defs_unchecked true [((Binding.name name, def),[])] thy'
   14.29          end) ak_names_types thy) ak_names_types thy4;
   14.30      
   14.31      (* proves that every atom-kind is an instance of at *)
   14.32 @@ -257,7 +257,7 @@
   14.33          val i_type = Type(ak_name_qu,[]);
   14.34          val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
   14.35          val at_type = Logic.mk_type i_type;
   14.36 -        val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy5)
   14.37 +        val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy5)
   14.38                                    ["at_def",
   14.39                                     ak_name ^ "_prm_" ^ ak_name ^ "_def",
   14.40                                     ak_name ^ "_prm_" ^ ak_name ^ ".simps",
   14.41 @@ -321,7 +321,7 @@
   14.42          val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   14.43          val pt_type = Logic.mk_type i_type1;
   14.44          val at_type = Logic.mk_type i_type2;
   14.45 -        val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy7)
   14.46 +        val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy7)
   14.47                                    ["pt_def",
   14.48                                     "pt_" ^ ak_name ^ "1",
   14.49                                     "pt_" ^ ak_name ^ "2",
   14.50 @@ -369,7 +369,7 @@
   14.51                                   (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   14.52           val fs_type = Logic.mk_type i_type1;
   14.53           val at_type = Logic.mk_type i_type2;
   14.54 -         val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy11)
   14.55 +         val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy11)
   14.56                                     ["fs_def",
   14.57                                      "fs_" ^ ak_name ^ "1"];
   14.58      
   14.59 @@ -422,8 +422,8 @@
   14.60               val at_type  = Logic.mk_type i_type1;
   14.61               val at_type' = Logic.mk_type i_type2;
   14.62               val cp_type  = Logic.mk_type i_type0;
   14.63 -             val simp_s   = HOL_basic_ss addsimps maps (PureThy.get_thms thy') ["cp_def"];
   14.64 -             val cp1      = PureThy.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1");
   14.65 +             val simp_s   = HOL_basic_ss addsimps maps (Global_Theory.get_thms thy') ["cp_def"];
   14.66 +             val cp1      = Global_Theory.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1");
   14.67  
   14.68               val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
   14.69               val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
   14.70 @@ -454,7 +454,7 @@
   14.71                             (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   14.72                   val at_type  = Logic.mk_type i_type1;
   14.73                   val at_type' = Logic.mk_type i_type2;
   14.74 -                 val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy')
   14.75 +                 val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy')
   14.76                                             ["disjoint_def",
   14.77                                              ak_name ^ "_prm_" ^ ak_name' ^ "_def",
   14.78                                              ak_name' ^ "_prm_" ^ ak_name ^ "_def"];
   14.79 @@ -493,7 +493,7 @@
   14.80           let
   14.81             val qu_name =  Sign.full_bname thy' ak_name';
   14.82             val cls_name = Sign.full_bname thy' ("pt_"^ak_name);
   14.83 -           val at_inst  = PureThy.get_thm thy' ("at_" ^ ak_name' ^ "_inst");
   14.84 +           val at_inst  = Global_Theory.get_thm thy' ("at_" ^ ak_name' ^ "_inst");
   14.85  
   14.86             val proof1 = EVERY [Class.intro_classes_tac [],
   14.87                                   rtac ((at_inst RS at_pt_inst) RS pt1) 1,
   14.88 @@ -501,7 +501,7 @@
   14.89                                   rtac ((at_inst RS at_pt_inst) RS pt3) 1,
   14.90                                   atac 1];
   14.91             val simp_s = HOL_basic_ss addsimps 
   14.92 -                        maps (PureThy.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"];  
   14.93 +                        maps (Global_Theory.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"];  
   14.94             val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
   14.95  
   14.96           in
   14.97 @@ -523,8 +523,8 @@
   14.98       val thy18 = fold (fn ak_name => fn thy =>
   14.99         let
  14.100            val cls_name = Sign.full_bname thy ("pt_"^ak_name);
  14.101 -          val at_thm   = PureThy.get_thm thy ("at_"^ak_name^"_inst");
  14.102 -          val pt_inst  = PureThy.get_thm thy ("pt_"^ak_name^"_inst");
  14.103 +          val at_thm   = Global_Theory.get_thm thy ("at_"^ak_name^"_inst");
  14.104 +          val pt_inst  = Global_Theory.get_thm thy ("pt_"^ak_name^"_inst");
  14.105  
  14.106            fun pt_proof thm = 
  14.107                EVERY [Class.intro_classes_tac [],
  14.108 @@ -571,11 +571,11 @@
  14.109             val proof =
  14.110                 (if ak_name = ak_name'
  14.111                  then
  14.112 -                  let val at_thm = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
  14.113 +                  let val at_thm = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst");
  14.114                    in  EVERY [Class.intro_classes_tac [],
  14.115                               rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
  14.116                  else
  14.117 -                  let val dj_inst = PureThy.get_thm thy' ("dj_"^ak_name'^"_"^ak_name);
  14.118 +                  let val dj_inst = Global_Theory.get_thm thy' ("dj_"^ak_name'^"_"^ak_name);
  14.119                        val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
  14.120                    in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end)
  14.121          in
  14.122 @@ -593,7 +593,7 @@
  14.123         val thy24 = fold (fn ak_name => fn thy => 
  14.124          let
  14.125            val cls_name = Sign.full_bname thy ("fs_"^ak_name);
  14.126 -          val fs_inst  = PureThy.get_thm thy ("fs_"^ak_name^"_inst");
  14.127 +          val fs_inst  = Global_Theory.get_thm thy ("fs_"^ak_name^"_inst");
  14.128            fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1];
  14.129  
  14.130            val fs_thm_unit  = fs_unit_inst;
  14.131 @@ -637,18 +637,18 @@
  14.132                val proof =
  14.133                  (if (ak_name'=ak_name'') then 
  14.134                    (let
  14.135 -                    val pt_inst  = PureThy.get_thm thy'' ("pt_"^ak_name''^"_inst");
  14.136 -                    val at_inst  = PureThy.get_thm thy'' ("at_"^ak_name''^"_inst");
  14.137 +                    val pt_inst  = Global_Theory.get_thm thy'' ("pt_"^ak_name''^"_inst");
  14.138 +                    val at_inst  = Global_Theory.get_thm thy'' ("at_"^ak_name''^"_inst");
  14.139                    in
  14.140                     EVERY [Class.intro_classes_tac [],
  14.141                            rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
  14.142                    end)
  14.143                  else
  14.144                    (let
  14.145 -                     val dj_inst  = PureThy.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name');
  14.146 +                     val dj_inst  = Global_Theory.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name');
  14.147                       val simp_s = HOL_basic_ss addsimps
  14.148                                          ((dj_inst RS dj_pp_forget)::
  14.149 -                                         (maps (PureThy.get_thms thy'')
  14.150 +                                         (maps (Global_Theory.get_thms thy'')
  14.151                                             [ak_name' ^"_prm_"^ak_name^"_def",
  14.152                                              ak_name''^"_prm_"^ak_name^"_def"]));
  14.153                    in
  14.154 @@ -671,9 +671,9 @@
  14.155          fold (fn ak_name' => fn thy' =>
  14.156          let
  14.157              val cls_name = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name');
  14.158 -            val cp_inst  = PureThy.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
  14.159 -            val pt_inst  = PureThy.get_thm thy' ("pt_"^ak_name^"_inst");
  14.160 -            val at_inst  = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
  14.161 +            val cp_inst  = Global_Theory.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
  14.162 +            val pt_inst  = Global_Theory.get_thm thy' ("pt_"^ak_name^"_inst");
  14.163 +            val at_inst  = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst");
  14.164  
  14.165              fun cp_proof thm  = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1];
  14.166            
  14.167 @@ -839,27 +839,27 @@
  14.168  
  14.169               
  14.170               (* list of all at_inst-theorems *)
  14.171 -             val ats = map (fn ak => PureThy.get_thm thy32 ("at_"^ak^"_inst")) ak_names
  14.172 +             val ats = map (fn ak => Global_Theory.get_thm thy32 ("at_"^ak^"_inst")) ak_names
  14.173               (* list of all pt_inst-theorems *)
  14.174 -             val pts = map (fn ak => PureThy.get_thm thy32 ("pt_"^ak^"_inst")) ak_names
  14.175 +             val pts = map (fn ak => Global_Theory.get_thm thy32 ("pt_"^ak^"_inst")) ak_names
  14.176               (* list of all cp_inst-theorems as a collection of lists*)
  14.177               val cps = 
  14.178 -                 let fun cps_fun ak1 ak2 =  PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")
  14.179 +                 let fun cps_fun ak1 ak2 =  Global_Theory.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")
  14.180                   in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; 
  14.181               (* list of all cp_inst-theorems that have different atom types *)
  14.182               val cps' = 
  14.183                  let fun cps'_fun ak1 ak2 = 
  14.184 -                if ak1=ak2 then NONE else SOME (PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
  14.185 +                if ak1=ak2 then NONE else SOME (Global_Theory.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
  14.186                  in map (fn aki => (map_filter I (map (cps'_fun aki) ak_names))) ak_names end;
  14.187               (* list of all dj_inst-theorems *)
  14.188               val djs = 
  14.189                 let fun djs_fun ak1 ak2 = 
  14.190 -                     if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 ("dj_"^ak2^"_"^ak1))
  14.191 +                     if ak1=ak2 then NONE else SOME(Global_Theory.get_thm thy32 ("dj_"^ak2^"_"^ak1))
  14.192                 in map_filter I (map_product djs_fun ak_names ak_names) end;
  14.193               (* list of all fs_inst-theorems *)
  14.194 -             val fss = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"_inst")) ak_names
  14.195 +             val fss = map (fn ak => Global_Theory.get_thm thy32 ("fs_"^ak^"_inst")) ak_names
  14.196               (* list of all at_inst-theorems *)
  14.197 -             val fs_axs = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"1")) ak_names
  14.198 +             val fs_axs = map (fn ak => Global_Theory.get_thm thy32 ("fs_"^ak^"1")) ak_names
  14.199  
  14.200               fun inst_pt thms = maps (fn ti => instR ti pts) thms;
  14.201               fun inst_at thms = maps (fn ti => instR ti ats) thms;
    15.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 20 15:29:53 2010 +0200
    15.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 20 16:05:25 2010 +0200
    15.3 @@ -306,7 +306,7 @@
    15.4      val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
    15.5  
    15.6      val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
    15.7 -    val perm_fun_def = PureThy.get_thm thy2 "perm_fun_def";
    15.8 +    val perm_fun_def = Global_Theory.get_thm thy2 "perm_fun_def";
    15.9  
   15.10      val unfolded_perm_eq_thms =
   15.11        if length descr = length new_type_names then []
   15.12 @@ -351,8 +351,8 @@
   15.13      val _ = warning "perm_append_thms";
   15.14  
   15.15      (*FIXME: these should be looked up statically*)
   15.16 -    val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst";
   15.17 -    val pt2 = PureThy.get_thm thy2 "pt2";
   15.18 +    val at_pt_inst = Global_Theory.get_thm thy2 "at_pt_inst";
   15.19 +    val pt2 = Global_Theory.get_thm thy2 "pt2";
   15.20  
   15.21      val perm_append_thms = maps (fn a =>
   15.22        let
   15.23 @@ -361,7 +361,7 @@
   15.24          val pi2 = Free ("pi2", permT);
   15.25          val pt_inst = pt_inst_of thy2 a;
   15.26          val pt2' = pt_inst RS pt2;
   15.27 -        val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
   15.28 +        val pt2_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
   15.29        in List.take (map Drule.export_without_context (split_conj_thm
   15.30          (Goal.prove_global thy2 [] []
   15.31             (augment_sort thy2 [pt_class_of thy2 a]
   15.32 @@ -384,8 +384,8 @@
   15.33  
   15.34      val _ = warning "perm_eq_thms";
   15.35  
   15.36 -    val pt3 = PureThy.get_thm thy2 "pt3";
   15.37 -    val pt3_rev = PureThy.get_thm thy2 "pt3_rev";
   15.38 +    val pt3 = Global_Theory.get_thm thy2 "pt3";
   15.39 +    val pt3_rev = Global_Theory.get_thm thy2 "pt3_rev";
   15.40  
   15.41      val perm_eq_thms = maps (fn a =>
   15.42        let
   15.43 @@ -396,7 +396,7 @@
   15.44          val pt_inst = pt_inst_of thy2 a;
   15.45          val pt3' = pt_inst RS pt3;
   15.46          val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
   15.47 -        val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
   15.48 +        val pt3_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
   15.49        in List.take (map Drule.export_without_context (split_conj_thm
   15.50          (Goal.prove_global thy2 [] []
   15.51            (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
   15.52 @@ -418,11 +418,11 @@
   15.53  
   15.54      (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
   15.55  
   15.56 -    val cp1 = PureThy.get_thm thy2 "cp1";
   15.57 -    val dj_cp = PureThy.get_thm thy2 "dj_cp";
   15.58 -    val pt_perm_compose = PureThy.get_thm thy2 "pt_perm_compose";
   15.59 -    val pt_perm_compose_rev = PureThy.get_thm thy2 "pt_perm_compose_rev";
   15.60 -    val dj_perm_perm_forget = PureThy.get_thm thy2 "dj_perm_perm_forget";
   15.61 +    val cp1 = Global_Theory.get_thm thy2 "cp1";
   15.62 +    val dj_cp = Global_Theory.get_thm thy2 "dj_cp";
   15.63 +    val pt_perm_compose = Global_Theory.get_thm thy2 "pt_perm_compose";
   15.64 +    val pt_perm_compose_rev = Global_Theory.get_thm thy2 "pt_perm_compose_rev";
   15.65 +    val dj_perm_perm_forget = Global_Theory.get_thm thy2 "dj_perm_perm_forget";
   15.66  
   15.67      fun composition_instance name1 name2 thy =
   15.68        let
   15.69 @@ -486,7 +486,7 @@
   15.70                   resolve_tac perm_eq_thms 1, assume_tac 1]) thy)
   15.71              (full_new_type_names' ~~ tyvars) thy
   15.72          end) atoms |>
   15.73 -      PureThy.add_thmss
   15.74 +      Global_Theory.add_thmss
   15.75          [((Binding.name (space_implode "_" new_type_names ^ "_unfolded_perm_eq"),
   15.76            unfolded_perm_eq_thms), [Simplifier.simp_add]),
   15.77           ((Binding.name (space_implode "_" new_type_names ^ "_perm_empty"),
   15.78 @@ -578,7 +578,7 @@
   15.79  
   15.80      val _ = warning "proving closure under permutation...";
   15.81  
   15.82 -    val abs_perm = PureThy.get_thms thy4 "abs_perm";
   15.83 +    val abs_perm = Global_Theory.get_thms thy4 "abs_perm";
   15.84  
   15.85      val perm_indnames' = map_filter
   15.86        (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
   15.87 @@ -626,7 +626,7 @@
   15.88            val pi = Free ("pi", permT);
   15.89            val T = Type (Sign.intern_type thy name, map TFree tvs);
   15.90          in apfst (pair r o hd)
   15.91 -          (PureThy.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals
   15.92 +          (Global_Theory.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals
   15.93              (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
   15.94               Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
   15.95                 (Const ("Nominal.perm", permT --> U --> U) $ pi $
   15.96 @@ -662,7 +662,7 @@
   15.97                asm_full_simp_tac (global_simpset_of thy addsimps [Rep_inverse]) 1,
   15.98                asm_full_simp_tac (global_simpset_of thy addsimps
   15.99                  [Rep RS perm_closed RS Abs_inverse]) 1,
  15.100 -              asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
  15.101 +              asm_full_simp_tac (HOL_basic_ss addsimps [Global_Theory.get_thm thy
  15.102                  ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
  15.103            end)
  15.104          (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
  15.105 @@ -801,7 +801,7 @@
  15.106          val def_name = (Long_Name.base_name cname) ^ "_def";
  15.107          val ([def_thm], thy') = thy |>
  15.108            Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
  15.109 -          (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
  15.110 +          (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
  15.111        in (thy', defs @ [def_thm], eqns @ [eqn]) end;
  15.112  
  15.113      fun dt_constr_defs ((((((_, (_, _, constrs)),
  15.114 @@ -935,8 +935,8 @@
  15.115      (** prove injectivity of constructors **)
  15.116  
  15.117      val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
  15.118 -    val alpha = PureThy.get_thms thy8 "alpha";
  15.119 -    val abs_fresh = PureThy.get_thms thy8 "abs_fresh";
  15.120 +    val alpha = Global_Theory.get_thms thy8 "alpha";
  15.121 +    val abs_fresh = Global_Theory.get_thms thy8 "abs_fresh";
  15.122  
  15.123      val pt_cp_sort =
  15.124        map (pt_class_of thy8) dt_atoms @
  15.125 @@ -1087,8 +1087,8 @@
  15.126  
  15.127      val indnames = Datatype_Prop.make_tnames recTs;
  15.128  
  15.129 -    val abs_supp = PureThy.get_thms thy8 "abs_supp";
  15.130 -    val supp_atm = PureThy.get_thms thy8 "supp_atm";
  15.131 +    val abs_supp = Global_Theory.get_thms thy8 "abs_supp";
  15.132 +    val supp_atm = Global_Theory.get_thms thy8 "supp_atm";
  15.133  
  15.134      val finite_supp_thms = map (fn atom =>
  15.135        let val atomT = Type (atom, [])
  15.136 @@ -1103,7 +1103,7 @@
  15.137             (fn _ => indtac dt_induct indnames 1 THEN
  15.138              ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps
  15.139                (abs_supp @ supp_atm @
  15.140 -               PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
  15.141 +               Global_Theory.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
  15.142                 flat supp_thms))))),
  15.143           length new_type_names))
  15.144        end) atoms;
  15.145 @@ -1117,8 +1117,8 @@
  15.146   
  15.147      val (_, thy9) = thy8 |>
  15.148        Sign.add_path big_name |>
  15.149 -      PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
  15.150 -      PureThy.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
  15.151 +      Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
  15.152 +      Global_Theory.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
  15.153        Sign.parent_path ||>>
  15.154        Datatype_Aux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
  15.155        Datatype_Aux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
  15.156 @@ -1235,17 +1235,17 @@
  15.157      val fin_set_fresh = map (fn s =>
  15.158        at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
  15.159      val pt1_atoms = map (fn Type (s, _) =>
  15.160 -      PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
  15.161 +      Global_Theory.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
  15.162      val pt2_atoms = map (fn Type (s, _) =>
  15.163 -      PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
  15.164 -    val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
  15.165 -    val fs_atoms = PureThy.get_thms thy9 "fin_supp";
  15.166 -    val abs_supp = PureThy.get_thms thy9 "abs_supp";
  15.167 -    val perm_fresh_fresh = PureThy.get_thms thy9 "perm_fresh_fresh";
  15.168 -    val calc_atm = PureThy.get_thms thy9 "calc_atm";
  15.169 -    val fresh_atm = PureThy.get_thms thy9 "fresh_atm";
  15.170 -    val fresh_left = PureThy.get_thms thy9 "fresh_left";
  15.171 -    val perm_swap = PureThy.get_thms thy9 "perm_swap";
  15.172 +      Global_Theory.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
  15.173 +    val exists_fresh' = Global_Theory.get_thms thy9 "exists_fresh'";
  15.174 +    val fs_atoms = Global_Theory.get_thms thy9 "fin_supp";
  15.175 +    val abs_supp = Global_Theory.get_thms thy9 "abs_supp";
  15.176 +    val perm_fresh_fresh = Global_Theory.get_thms thy9 "perm_fresh_fresh";
  15.177 +    val calc_atm = Global_Theory.get_thms thy9 "calc_atm";
  15.178 +    val fresh_atm = Global_Theory.get_thms thy9 "fresh_atm";
  15.179 +    val fresh_left = Global_Theory.get_thms thy9 "fresh_left";
  15.180 +    val perm_swap = Global_Theory.get_thms thy9 "perm_swap";
  15.181  
  15.182      fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
  15.183        let
  15.184 @@ -1408,9 +1408,9 @@
  15.185  
  15.186      val (_, thy10) = thy9 |>
  15.187        Sign.add_path big_name |>
  15.188 -      PureThy.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
  15.189 -      PureThy.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
  15.190 -      PureThy.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
  15.191 +      Global_Theory.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
  15.192 +      Global_Theory.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
  15.193 +      Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
  15.194  
  15.195      (**** recursion combinator ****)
  15.196  
  15.197 @@ -1517,13 +1517,13 @@
  15.198            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
  15.199            (map dest_Free rec_fns)
  15.200            (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
  15.201 -      ||> PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
  15.202 +      ||> Global_Theory.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
  15.203        ||> Sign.restore_naming thy10;
  15.204  
  15.205      (** equivariance **)
  15.206  
  15.207 -    val fresh_bij = PureThy.get_thms thy11 "fresh_bij";
  15.208 -    val perm_bij = PureThy.get_thms thy11 "perm_bij";
  15.209 +    val fresh_bij = Global_Theory.get_thms thy11 "fresh_bij";
  15.210 +    val perm_bij = Global_Theory.get_thms thy11 "perm_bij";
  15.211  
  15.212      val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT =>
  15.213        let
  15.214 @@ -1565,7 +1565,7 @@
  15.215      val rec_fin_supp_thms = map (fn aT =>
  15.216        let
  15.217          val name = Long_Name.base_name (fst (dest_Type aT));
  15.218 -        val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
  15.219 +        val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
  15.220          val aset = HOLogic.mk_setT aT;
  15.221          val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
  15.222          val fins = map (fn (f, T) => HOLogic.mk_Trueprop
  15.223 @@ -1604,7 +1604,7 @@
  15.224      val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
  15.225        let
  15.226          val name = Long_Name.base_name (fst (dest_Type aT));
  15.227 -        val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
  15.228 +        val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
  15.229          val a = Free ("a", aT);
  15.230          val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
  15.231            (fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts)
  15.232 @@ -2018,7 +2018,7 @@
  15.233        |> Sign.add_consts_i (map (fn ((name, T), T') =>
  15.234            (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
  15.235            (reccomb_names ~~ recTs ~~ rec_result_Ts))
  15.236 -      |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
  15.237 +      |> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
  15.238            (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
  15.239             Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
  15.240               set $ Free ("x", T) $ Free ("y", T'))))))
  15.241 @@ -2055,7 +2055,7 @@
  15.242  
  15.243      (* FIXME: theorems are stored in database for testing only *)
  15.244      val (_, thy13) = thy12 |>
  15.245 -      PureThy.add_thmss
  15.246 +      Global_Theory.add_thmss
  15.247          [((Binding.name "rec_equiv", flat rec_equiv_thms), []),
  15.248           ((Binding.name "rec_equiv'", flat rec_equiv_thms'), []),
  15.249           ((Binding.name "rec_fin_supp", flat rec_fin_supp_thms), []),
    16.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Sep 20 15:29:53 2010 +0200
    16.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Sep 20 16:05:25 2010 +0200
    16.3 @@ -37,7 +37,7 @@
    16.4    res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th);
    16.5  
    16.6  fun get_dyn_thm thy name atom_name =
    16.7 -  PureThy.get_thm thy name handle ERROR _ =>
    16.8 +  Global_Theory.get_thm thy name handle ERROR _ =>
    16.9      error ("The atom type "^atom_name^" is not defined.");
   16.10  
   16.11  (* End of function waiting to be in the library :o) *)
   16.12 @@ -126,8 +126,8 @@
   16.13      val thy = theory_of_thm thm;
   16.14      val ctxt = ProofContext.init_global thy;
   16.15      val ss = global_simpset_of thy;
   16.16 -    val abs_fresh = PureThy.get_thms thy "abs_fresh";
   16.17 -    val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
   16.18 +    val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
   16.19 +    val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
   16.20      val ss' = ss addsimps fresh_prod::abs_fresh;
   16.21      val ss'' = ss' addsimps fresh_perm_app;
   16.22      val x = hd (tl (OldTerm.term_vars (prop_of exI)));
    17.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon Sep 20 15:29:53 2010 +0200
    17.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Sep 20 16:05:25 2010 +0200
    17.3 @@ -271,21 +271,21 @@
    17.4             (NominalDatatype.fresh_const U T $ u $ t)) bvars)
    17.5               (ts ~~ binder_types (fastype_of p)))) prems;
    17.6  
    17.7 -    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    17.8 -    val pt2_atoms = map (fn aT => PureThy.get_thm thy
    17.9 +    val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
   17.10 +    val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
   17.11        ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
   17.12      val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
   17.13        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
   17.14        addsimprocs [mk_perm_bool_simproc ["Fun.id"],
   17.15          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
   17.16 -    val fresh_bij = PureThy.get_thms thy "fresh_bij";
   17.17 -    val perm_bij = PureThy.get_thms thy "perm_bij";
   17.18 -    val fs_atoms = map (fn aT => PureThy.get_thm thy
   17.19 +    val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
   17.20 +    val perm_bij = Global_Theory.get_thms thy "perm_bij";
   17.21 +    val fs_atoms = map (fn aT => Global_Theory.get_thm thy
   17.22        ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
   17.23 -    val exists_fresh' = PureThy.get_thms thy "exists_fresh'";
   17.24 -    val fresh_atm = PureThy.get_thms thy "fresh_atm";
   17.25 -    val swap_simps = PureThy.get_thms thy "swap_simps";
   17.26 -    val perm_fresh_fresh = PureThy.get_thms thy "perm_fresh_fresh";
   17.27 +    val exists_fresh' = Global_Theory.get_thms thy "exists_fresh'";
   17.28 +    val fresh_atm = Global_Theory.get_thms thy "fresh_atm";
   17.29 +    val swap_simps = Global_Theory.get_thms thy "swap_simps";
   17.30 +    val perm_fresh_fresh = Global_Theory.get_thms thy "perm_fresh_fresh";
   17.31  
   17.32      fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) =
   17.33        let
   17.34 @@ -610,7 +610,7 @@
   17.35             | xs => error ("No such atoms: " ^ commas xs);
   17.36           atoms)
   17.37        end;
   17.38 -    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
   17.39 +    val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
   17.40      val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
   17.41        (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
   17.42        [mk_perm_bool_simproc names,
    18.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Mon Sep 20 15:29:53 2010 +0200
    18.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Sep 20 16:05:25 2010 +0200
    18.3 @@ -290,14 +290,14 @@
    18.4             HOLogic.mk_setT U --> HOLogic.boolT) $ u)) sets) |>
    18.5        split_list) prems |> split_list;
    18.6  
    18.7 -    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    18.8 -    val pt2_atoms = map (fn a => PureThy.get_thm thy
    18.9 +    val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
   18.10 +    val pt2_atoms = map (fn a => Global_Theory.get_thm thy
   18.11        ("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
   18.12      val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
   18.13        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
   18.14        addsimprocs [mk_perm_bool_simproc ["Fun.id"],
   18.15          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
   18.16 -    val fresh_star_bij = PureThy.get_thms thy "fresh_star_bij";
   18.17 +    val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
   18.18      val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
   18.19      val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
   18.20      val dj_thms = maps (fn a =>
   18.21 @@ -319,7 +319,7 @@
   18.22          val p = foldr1 HOLogic.mk_prod (map protect ts);
   18.23          val atom = fst (dest_Type T);
   18.24          val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
   18.25 -        val fs_atom = PureThy.get_thm thy
   18.26 +        val fs_atom = Global_Theory.get_thm thy
   18.27            ("fs_" ^ Long_Name.base_name atom ^ "1");
   18.28          val avoid_th = Drule.instantiate'
   18.29            [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)]
    19.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Mon Sep 20 15:29:53 2010 +0200
    19.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Sep 20 16:05:25 2010 +0200
    19.3 @@ -71,8 +71,8 @@
    19.4  val supports_fresh_rule = @{thm "supports_fresh"};
    19.5  
    19.6  (* pulls out dynamically a thm via the proof state *)
    19.7 -fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) name;
    19.8 -fun dynamic_thm  st name = PureThy.get_thm  (theory_of_thm st) name;
    19.9 +fun dynamic_thms st name = Global_Theory.get_thms (theory_of_thm st) name;
   19.10 +fun dynamic_thm  st name = Global_Theory.get_thm  (theory_of_thm st) name;
   19.11  
   19.12  
   19.13  (* needed in the process of fully simplifying permutations *)
   19.14 @@ -107,8 +107,8 @@
   19.15              (if (applicable_app f) then
   19.16                let
   19.17                  val name = Long_Name.base_name n
   19.18 -                val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst")
   19.19 -                val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst")
   19.20 +                val at_inst = Global_Theory.get_thm sg ("at_" ^ name ^ "_inst")
   19.21 +                val pt_inst = Global_Theory.get_thm sg ("pt_" ^ name ^ "_inst")
   19.22                in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
   19.23              else NONE)
   19.24        | _ => NONE
   19.25 @@ -202,13 +202,13 @@
   19.26            SOME (Drule.instantiate'
   19.27              [SOME (ctyp_of sg (fastype_of t))]
   19.28              [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
   19.29 -            (mk_meta_eq ([PureThy.get_thm sg ("pt_"^tname'^"_inst"),
   19.30 -             PureThy.get_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
   19.31 +            (mk_meta_eq ([Global_Theory.get_thm sg ("pt_"^tname'^"_inst"),
   19.32 +             Global_Theory.get_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
   19.33          else
   19.34            SOME (Drule.instantiate'
   19.35              [SOME (ctyp_of sg (fastype_of t))]
   19.36              [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
   19.37 -            (mk_meta_eq (PureThy.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS 
   19.38 +            (mk_meta_eq (Global_Theory.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS 
   19.39               cp1_aux)))
   19.40        else NONE
   19.41      end
    20.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Mon Sep 20 15:29:53 2010 +0200
    20.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Mon Sep 20 16:05:25 2010 +0200
    20.3 @@ -56,7 +56,7 @@
    20.4      val mypi = Thm.cterm_of thy pi
    20.5      val T = fastype_of pi'
    20.6      val mypifree = Thm.cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi')
    20.7 -    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"
    20.8 +    val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"
    20.9    in
   20.10      EVERY1 [tactic ctxt ("iffI applied", rtac @{thm iffI}),
   20.11              tactic ctxt ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
   20.12 @@ -175,7 +175,7 @@
   20.13     "equivariance theorem declaration" #>
   20.14    Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
   20.15      "equivariance theorem declaration (without checking the form of the lemma)" #>
   20.16 -  PureThy.add_thms_dynamic (@{binding eqvts}, Data.get);
   20.17 +  Global_Theory.add_thms_dynamic (@{binding eqvts}, Data.get);
   20.18  
   20.19  
   20.20  end;
    21.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Mon Sep 20 15:29:53 2010 +0200
    21.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Mon Sep 20 16:05:25 2010 +0200
    21.3 @@ -671,7 +671,7 @@
    21.4  
    21.5  setup {*
    21.6  Theory.add_consts_i const_decls
    21.7 -#> (fn thy  => let val ([thm],thy') = PureThy.add_axioms [(("dist_axiom",dist),[])] thy
    21.8 +#> (fn thy  => let val ([thm],thy') = Global_Theory.add_axioms [(("dist_axiom",dist),[])] thy
    21.9                 in (da := thm; thy') end)
   21.10  *}
   21.11  
    22.1 --- a/src/HOL/String.thy	Mon Sep 20 15:29:53 2010 +0200
    22.2 +++ b/src/HOL/String.thy	Mon Sep 20 16:05:25 2010 +0200
    22.3 @@ -53,7 +53,8 @@
    22.4     (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
    22.5        nibbles nibbles;
    22.6  in
    22.7 -  PureThy.note_thmss Thm.definitionK [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
    22.8 +  Global_Theory.note_thmss Thm.definitionK
    22.9 +    [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
   22.10    #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
   22.11  end
   22.12  *}
    23.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 20 15:29:53 2010 +0200
    23.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 20 16:05:25 2010 +0200
    23.3 @@ -241,7 +241,7 @@
    23.4          val ([def_thm], thy') =
    23.5            thy
    23.6            |> Sign.add_consts_i [(cname', constrT, mx)]
    23.7 -          |> (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
    23.8 +          |> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
    23.9  
   23.10        in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
   23.11  
   23.12 @@ -352,7 +352,7 @@
   23.13            Logic.mk_equals (Const (iso_name, T --> Univ_elT),
   23.14              list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
   23.15          val (def_thms, thy') =
   23.16 -          apsnd Theory.checkpoint ((PureThy.add_defs false o map Thm.no_attributes) defs thy);
   23.17 +          apsnd Theory.checkpoint ((Global_Theory.add_defs false o map Thm.no_attributes) defs thy);
   23.18  
   23.19          (* prove characteristic equations *)
   23.20  
   23.21 @@ -628,7 +628,7 @@
   23.22      val ([dt_induct'], thy7) =
   23.23        thy6
   23.24        |> Sign.add_path big_name
   23.25 -      |> PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
   23.26 +      |> Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
   23.27        ||> Sign.parent_path
   23.28        ||> Theory.checkpoint;
   23.29  
    24.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Sep 20 15:29:53 2010 +0200
    24.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Sep 20 16:05:25 2010 +0200
    24.3 @@ -234,11 +234,13 @@
    24.4        |> Sign.add_consts_i (map (fn ((name, T), T') =>
    24.5            (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
    24.6            (reccomb_names ~~ recTs ~~ rec_result_Ts))
    24.7 -      |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    24.8 -          (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
    24.9 -           Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   24.10 -             set $ Free ("x", T) $ Free ("y", T'))))))
   24.11 -               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
   24.12 +      |> (Global_Theory.add_defs false o map Thm.no_attributes)
   24.13 +          (map (fn ((((name, comb), set), T), T') =>
   24.14 +            (Binding.name (Long_Name.base_name name ^ "_def"),
   24.15 +              Logic.mk_equals (comb, absfree ("x", T,
   24.16 +               Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   24.17 +                 set $ Free ("x", T) $ Free ("y", T'))))))
   24.18 +                   (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
   24.19        ||> Sign.parent_path
   24.20        ||> Theory.checkpoint;
   24.21  
   24.22 @@ -259,7 +261,7 @@
   24.23    in
   24.24      thy2
   24.25      |> Sign.add_path (space_implode "_" new_type_names)
   24.26 -    |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])]
   24.27 +    |> Global_Theory.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])]
   24.28      ||> Sign.parent_path
   24.29      ||> Theory.checkpoint
   24.30      |-> (fn thms => pair (reccomb_names, flat thms))
   24.31 @@ -319,7 +321,7 @@
   24.32            val ([def_thm], thy') =
   24.33              thy
   24.34              |> Sign.declare_const decl |> snd
   24.35 -            |> (PureThy.add_defs false o map Thm.no_attributes) [def];
   24.36 +            |> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
   24.37  
   24.38          in (defs @ [def_thm], thy')
   24.39          end) (hd descr ~~ newTs ~~ case_names ~~
    25.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 20 15:29:53 2010 +0200
    25.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 20 16:05:25 2010 +0200
    25.3 @@ -99,7 +99,7 @@
    25.4  fun store_thmss_atts label tnames attss thmss =
    25.5    fold_map (fn ((tname, atts), thms) =>
    25.6      Sign.add_path tname
    25.7 -    #> PureThy.add_thmss [((Binding.name label, thms), atts)]
    25.8 +    #> Global_Theory.add_thmss [((Binding.name label, thms), atts)]
    25.9      #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
   25.10    ##> Theory.checkpoint;
   25.11  
   25.12 @@ -108,7 +108,7 @@
   25.13  fun store_thms_atts label tnames attss thmss =
   25.14    fold_map (fn ((tname, atts), thms) =>
   25.15      Sign.add_path tname
   25.16 -    #> PureThy.add_thms [((Binding.name label, thms), atts)]
   25.17 +    #> Global_Theory.add_thms [((Binding.name label, thms), atts)]
   25.18      #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
   25.19    ##> Theory.checkpoint;
   25.20  
    26.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Sep 20 15:29:53 2010 +0200
    26.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Sep 20 16:05:25 2010 +0200
    26.3 @@ -109,7 +109,7 @@
    26.4      fun add_eq_thms tyco =
    26.5        Theory.checkpoint
    26.6        #> `(fn thy => mk_eq_eqns thy tyco)
    26.7 -      #-> (fn (thms, thm) => PureThy.note_thmss Thm.lemmaK
    26.8 +      #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
    26.9            [((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
   26.10              ((prefix tyco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
   26.11        #> snd
    27.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Sep 20 15:29:53 2010 +0200
    27.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Sep 20 16:05:25 2010 +0200
    27.3 @@ -334,7 +334,7 @@
    27.4          (drop (length dt_names) inducts);
    27.5    in
    27.6      thy9
    27.7 -    |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
    27.8 +    |> Global_Theory.add_thmss ([((prfx (Binding.name "simps"), simps), []),
    27.9          ((prfx (Binding.name "inducts"), inducts), []),
   27.10          ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
   27.11          ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites),
   27.12 @@ -367,7 +367,8 @@
   27.13        |> store_thmss "inject" new_type_names raw_inject
   27.14        ||>> store_thmss "distinct" new_type_names raw_distinct
   27.15        ||> Sign.add_path (space_implode "_" new_type_names)
   27.16 -      ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
   27.17 +      ||>> Global_Theory.add_thms
   27.18 +        [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
   27.19        ||> Sign.restore_naming thy1;
   27.20    in
   27.21      thy2
    28.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Sep 20 15:29:53 2010 +0200
    28.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Sep 20 16:05:25 2010 +0200
    28.3 @@ -122,7 +122,7 @@
    28.4      val vs = map (fn i => List.nth (pnames, i)) is;
    28.5      val (thm', thy') = thy
    28.6        |> Sign.root_path
    28.7 -      |> PureThy.store_thm
    28.8 +      |> Global_Theory.store_thm
    28.9          (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
   28.10        ||> Sign.restore_naming thy;
   28.11  
   28.12 @@ -193,7 +193,7 @@
   28.13      val exh_name = Thm.derivation_name exhaust;
   28.14      val (thm', thy') = thy
   28.15        |> Sign.root_path
   28.16 -      |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
   28.17 +      |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
   28.18        ||> Sign.restore_naming thy;
   28.19  
   28.20      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    29.1 --- a/src/HOL/Tools/Function/size.ML	Mon Sep 20 15:29:53 2010 +0200
    29.2 +++ b/src/HOL/Tools/Function/size.ML	Mon Sep 20 16:05:25 2010 +0200
    29.3 @@ -142,7 +142,7 @@
    29.4        |> Sign.add_consts_i (map (fn (s, T) =>
    29.5             (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
    29.6             (size_names ~~ recTs1))
    29.7 -      |> PureThy.add_defs false
    29.8 +      |> Global_Theory.add_defs false
    29.9          (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
   29.10             (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
   29.11        ||> Class.instantiation
   29.12 @@ -207,11 +207,12 @@
   29.13      val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
   29.14        prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3;
   29.15  
   29.16 -    val ([size_thms], thy'') =  PureThy.add_thmss
   29.17 -      [((Binding.name "size", size_eqns),
   29.18 -        [Simplifier.simp_add, Nitpick_Simps.add,
   29.19 -         Thm.declaration_attribute
   29.20 -             (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
   29.21 +    val ([size_thms], thy'') =
   29.22 +      Global_Theory.add_thmss
   29.23 +        [((Binding.name "size", size_eqns),
   29.24 +          [Simplifier.simp_add, Nitpick_Simps.add,
   29.25 +           Thm.declaration_attribute
   29.26 +               (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy';
   29.27  
   29.28    in
   29.29      SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
    30.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Sep 20 15:29:53 2010 +0200
    30.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Sep 20 16:05:25 2010 +0200
    30.3 @@ -1303,7 +1303,7 @@
    30.4        List.partition (is_typedef_axiom ctxt false) user_nondefs
    30.5        |>> append built_in_nondefs
    30.6      val defs =
    30.7 -      (thy |> PureThy.all_thms_of
    30.8 +      (thy |> Global_Theory.all_thms_of
    30.9             |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
   30.10             |> map (prop_of o snd)
   30.11             |> filter_out is_trivial_definition
   30.12 @@ -1867,7 +1867,7 @@
   30.13  fun ground_theorem_table thy =
   30.14    fold ((fn @{const Trueprop} $ t1 =>
   30.15              is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
   30.16 -          | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
   30.17 +          | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy) Inttab.empty
   30.18  
   30.19  (* TODO: Move to "Nitpick.thy" *)
   30.20  val basic_ersatz_table =
    31.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Sep 20 15:29:53 2010 +0200
    31.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Sep 20 16:05:25 2010 +0200
    31.3 @@ -2158,15 +2158,15 @@
    31.4          val def = Logic.mk_equals (lhs, predterm)
    31.5          val ([definition], thy') = thy |>
    31.6            Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
    31.7 -          PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
    31.8 +          Global_Theory.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
    31.9          val ctxt' = ProofContext.init_global thy'
   31.10          val rules as ((intro, elim), _) =
   31.11            create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
   31.12          in thy'
   31.13            |> set_function_name Pred name mode mode_cname
   31.14            |> add_predfun_data name mode (definition, rules)
   31.15 -          |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
   31.16 -          |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
   31.17 +          |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
   31.18 +          |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
   31.19            |> Theory.checkpoint
   31.20          end;
   31.21    in
   31.22 @@ -2883,7 +2883,7 @@
   31.23        (fn thm => Context.mapping (Code.add_eqn thm) I))))
   31.24      val thy''' =
   31.25        Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
   31.26 -      fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
   31.27 +      fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
   31.28        [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
   31.29          [attrib thy ])] thy))
   31.30        result_thms' thy'' |> Theory.checkpoint)
    32.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Sep 20 15:29:53 2010 +0200
    32.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Sep 20 16:05:25 2010 +0200
    32.3 @@ -108,7 +108,7 @@
    32.4        val def = Logic.mk_equals (lhs, atom)
    32.5        val ([definition], thy') = thy
    32.6          |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
    32.7 -        |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
    32.8 +        |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
    32.9      in
   32.10        (lhs, ((full_constname, [definition]) :: defs, thy'))
   32.11      end
   32.12 @@ -327,7 +327,7 @@
   32.13              val def = Logic.mk_equals (lhs, abs_arg')
   32.14              val ([definition], thy') = thy
   32.15                |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
   32.16 -              |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
   32.17 +              |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
   32.18            in
   32.19              (list_comb (Logic.varify_global const, vars),
   32.20                ((full_constname, [definition])::new_defs, thy'))
    33.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Sep 20 15:29:53 2010 +0200
    33.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Sep 20 16:05:25 2010 +0200
    33.3 @@ -57,7 +57,7 @@
    33.4  
    33.5  val z3_rules_setup =
    33.6    Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
    33.7 -  PureThy.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
    33.8 +  Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
    33.9  
   33.10  end
   33.11  
    34.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Sep 20 15:29:53 2010 +0200
    34.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Sep 20 16:05:25 2010 +0200
    34.3 @@ -708,7 +708,7 @@
    34.4  fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths =
    34.5    let
    34.6      val thy = ProofContext.theory_of ctxt
    34.7 -    val global_facts = PureThy.facts_of thy
    34.8 +    val global_facts = Global_Theory.facts_of thy
    34.9      val local_facts = ProofContext.facts_of ctxt
   34.10      val named_locals = local_facts |> Facts.dest_static []
   34.11      val assms = Assumption.all_assms_of ctxt
    35.1 --- a/src/HOL/Tools/TFL/tfl.ML	Mon Sep 20 15:29:53 2010 +0200
    35.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Mon Sep 20 16:05:25 2010 +0200
    35.3 @@ -382,7 +382,7 @@
    35.4                        $ functional
    35.5       val def_term = const_def thy (fid, Ty, wfrec_R_M)
    35.6       val ([def], thy') =
    35.7 -      PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
    35.8 +      Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
    35.9   in (thy', def) end;
   35.10  end;
   35.11  
   35.12 @@ -539,7 +539,7 @@
   35.13       val defn = const_def thy (name, Ty, S.list_mk_abs (args,rhs))
   35.14       val ([def0], theory) =
   35.15         thy
   35.16 -       |> PureThy.add_defs false
   35.17 +       |> Global_Theory.add_defs false
   35.18              [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
   35.19       val def = Thm.unvarify_global def0;
   35.20       val dummy =
    36.1 --- a/src/HOL/Tools/choice_specification.ML	Mon Sep 20 15:29:53 2010 +0200
    36.2 +++ b/src/HOL/Tools/choice_specification.ML	Mon Sep 20 16:05:25 2010 +0200
    36.3 @@ -33,7 +33,7 @@
    36.4                                 else thname
    36.5                  val def_eq = Logic.mk_equals (Const(cname_full,ctype),
    36.6                                                HOLogic.choice_const ctype $  P)
    36.7 -                val (thms, thy') = PureThy.add_defs covld [((Binding.name cdefname, def_eq),[])] thy
    36.8 +                val (thms, thy') = Global_Theory.add_defs covld [((Binding.name cdefname, def_eq),[])] thy
    36.9                  val thm' = [thm,hd thms] MRS @{thm exE_some}
   36.10              in
   36.11                  mk_definitional cos (thy',thm')
   36.12 @@ -189,7 +189,7 @@
   36.13                              if name = ""
   36.14                              then arg |> Library.swap
   36.15                              else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
   36.16 -                                  PureThy.store_thm (Binding.name name, thm) thy)
   36.17 +                                  Global_Theory.store_thm (Binding.name name, thm) thy)
   36.18                      in
   36.19                          args |> apsnd (remove_alls frees)
   36.20                               |> apsnd undo_imps
    37.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Sep 20 15:29:53 2010 +0200
    37.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Sep 20 16:05:25 2010 +0200
    37.3 @@ -273,7 +273,7 @@
    37.4  fun add_ind_realizer rsets intrs induct raw_induct elims vs thy =
    37.5    let
    37.6      val qualifier = Long_Name.qualifier (name_of_thm induct);
    37.7 -    val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
    37.8 +    val inducts = Global_Theory.get_thms thy (Long_Name.qualify qualifier "inducts");
    37.9      val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
   37.10      val ar = length vs + length iTs;
   37.11      val params = Inductive.params_of raw_induct;
   37.12 @@ -356,7 +356,7 @@
   37.13             subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
   37.14               (rintrs ~~ maps snd rss)) [] ||>
   37.15        Sign.root_path;
   37.16 -    val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
   37.17 +    val thy3 = fold (Global_Theory.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
   37.18  
   37.19      (** realizer for induction rule **)
   37.20  
   37.21 @@ -395,11 +395,11 @@
   37.22             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
   37.23               [K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac,
   37.24                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
   37.25 -        val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
   37.26 +        val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
   37.27            (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
   37.28          val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
   37.29            (Datatype_Aux.split_conj_thm thm');
   37.30 -        val ([thms'], thy'') = PureThy.add_thmss
   37.31 +        val ([thms'], thy'') = Global_Theory.add_thmss
   37.32            [((Binding.qualified_name (space_implode "_"
   37.33               (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @
   37.34                 ["correctness"])), thms), [])] thy';
   37.35 @@ -454,7 +454,7 @@
   37.36             rewrite_goals_tac rews,
   37.37             REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
   37.38               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
   37.39 -        val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
   37.40 +        val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
   37.41            (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
   37.42        in
   37.43          Extraction.add_realizers_i
    38.1 --- a/src/HOL/Tools/old_primrec.ML	Mon Sep 20 15:29:53 2010 +0200
    38.2 +++ b/src/HOL/Tools/old_primrec.ML	Mon Sep 20 16:05:25 2010 +0200
    38.3 @@ -308,11 +308,11 @@
    38.4    end;
    38.5  
    38.6  fun thy_note ((name, atts), thms) =
    38.7 -  PureThy.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms));
    38.8 +  Global_Theory.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms));
    38.9  fun thy_def false ((name, atts), t) =
   38.10 -      PureThy.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm))
   38.11 +      Global_Theory.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm))
   38.12    | thy_def true ((name, atts), t) =
   38.13 -      PureThy.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm));
   38.14 +      Global_Theory.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm));
   38.15  
   38.16  in
   38.17  
    39.1 --- a/src/HOL/Tools/recdef.ML	Mon Sep 20 15:29:53 2010 +0200
    39.2 +++ b/src/HOL/Tools/recdef.ML	Mon Sep 20 16:05:25 2010 +0200
    39.3 @@ -208,9 +208,9 @@
    39.4      val ((simps' :: rules', [induct']), thy) =
    39.5        thy
    39.6        |> Sign.add_path bname
    39.7 -      |> PureThy.add_thmss
    39.8 +      |> Global_Theory.add_thmss
    39.9          (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
   39.10 -      ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]
   39.11 +      ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
   39.12        ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
   39.13      val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
   39.14      val thy =
   39.15 @@ -239,7 +239,7 @@
   39.16      val ([induct_rules'], thy3) =
   39.17        thy2
   39.18        |> Sign.add_path bname
   39.19 -      |> PureThy.add_thms [((Binding.name "induct_rules", induct_rules), [])]
   39.20 +      |> Global_Theory.add_thms [((Binding.name "induct_rules", induct_rules), [])]
   39.21        ||> Sign.parent_path;
   39.22    in (thy3, {induct_rules = induct_rules'}) end;
   39.23  
    40.1 --- a/src/HOL/Tools/record.ML	Mon Sep 20 15:29:53 2010 +0200
    40.2 +++ b/src/HOL/Tools/record.ML	Mon Sep 20 16:05:25 2010 +0200
    40.3 @@ -153,7 +153,7 @@
    40.4      val ([isom_def], cdef_thy) =
    40.5        typ_thy
    40.6        |> Sign.declare_const ((isom_binding, isomT), NoSyn) |> snd
    40.7 -      |> PureThy.add_defs false
    40.8 +      |> Global_Theory.add_defs false
    40.9          [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
   40.10  
   40.11      val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
   40.12 @@ -1658,7 +1658,7 @@
   40.13      fun mk_defs () =
   40.14        typ_thy
   40.15        |> Sign.declare_const ((ext_binding, ext_type), NoSyn) |> snd
   40.16 -      |> PureThy.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
   40.17 +      |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
   40.18        ||> Theory.checkpoint
   40.19      val ([ext_def], defs_thy) =
   40.20        timeit_msg "record extension constructor def:" mk_defs;
   40.21 @@ -1749,7 +1749,7 @@
   40.22  
   40.23      val ([induct', inject', surjective', split_meta'], thm_thy) =
   40.24        defs_thy
   40.25 -      |> PureThy.add_thms (map (Thm.no_attributes o apfst Binding.name)
   40.26 +      |> Global_Theory.add_thms (map (Thm.no_attributes o apfst Binding.name)
   40.27             [("ext_induct", induct),
   40.28              ("ext_inject", inject),
   40.29              ("ext_surjective", surject),
   40.30 @@ -2096,11 +2096,12 @@
   40.31          (sel_decls ~~ (field_syntax @ [NoSyn]))
   40.32        |> fold (fn (x, T) => snd o Sign.declare_const ((Binding.name x, T), NoSyn))
   40.33          (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
   40.34 -      |> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
   40.35 -        sel_specs
   40.36 -      ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
   40.37 -        upd_specs
   40.38 -      ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
   40.39 +      |> (Global_Theory.add_defs false o
   40.40 +            map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
   40.41 +      ||>> (Global_Theory.add_defs false o
   40.42 +            map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
   40.43 +      ||>> (Global_Theory.add_defs false o
   40.44 +            map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
   40.45          [make_spec, fields_spec, extend_spec, truncate_spec]
   40.46        ||> Theory.checkpoint
   40.47      val (((sel_defs, upd_defs), derived_defs), defs_thy) =
   40.48 @@ -2339,7 +2340,7 @@
   40.49            [surjective', equality']),
   40.50            [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
   40.51        defs_thy
   40.52 -      |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
   40.53 +      |> (Global_Theory.add_thmss o map (Thm.no_attributes o apfst Binding.name))
   40.54           [("select_convs", sel_convs_standard),
   40.55            ("update_convs", upd_convs_standard),
   40.56            ("select_defs", sel_defs),
   40.57 @@ -2348,10 +2349,10 @@
   40.58            ("unfold_congs", unfold_congs),
   40.59            ("splits", [split_meta_standard, split_object, split_ex]),
   40.60            ("defs", derived_defs)]
   40.61 -      ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
   40.62 +      ||>> (Global_Theory.add_thms o map (Thm.no_attributes o apfst Binding.name))
   40.63            [("surjective", surjective),
   40.64             ("equality", equality)]
   40.65 -      ||>> (PureThy.add_thms o (map o apfst o apfst) Binding.name)
   40.66 +      ||>> (Global_Theory.add_thms o (map o apfst o apfst) Binding.name)
   40.67          [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
   40.68           (("induct", induct), induct_type_global name),
   40.69           (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
   40.70 @@ -2364,7 +2365,7 @@
   40.71  
   40.72      val ([simps', iffs'], thms_thy') =
   40.73        thms_thy
   40.74 -      |> PureThy.add_thmss
   40.75 +      |> Global_Theory.add_thmss
   40.76            [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
   40.77             ((Binding.name "iffs", iffs), [iff_add])];
   40.78  
    41.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon Sep 20 15:29:53 2010 +0200
    41.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon Sep 20 16:05:25 2010 +0200
    41.3 @@ -63,7 +63,7 @@
    41.4        (Binding.suffix_name "_def" b, Logic.mk_equals (c, t));
    41.5      val defs = map2 mk_def consts specs;
    41.6      val (def_thms, thy) =
    41.7 -      PureThy.add_defs false (map Thm.no_attributes defs) thy;
    41.8 +      Global_Theory.add_defs false (map Thm.no_attributes defs) thy;
    41.9    in
   41.10      ((consts, def_thms), thy)
   41.11    end;
    42.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Sep 20 15:29:53 2010 +0200
    42.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Sep 20 16:05:25 2010 +0200
    42.3 @@ -194,7 +194,7 @@
    42.4            ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
    42.5    in
    42.6      theorems_thy
    42.7 -      |> PureThy.add_thmss
    42.8 +      |> Global_Theory.add_thmss
    42.9             [((Binding.qualified true "rews" comp_dbind,
   42.10                flat rewss @ take_rews), [])]
   42.11        |> snd
    43.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Sep 20 15:29:53 2010 +0200
    43.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Sep 20 16:05:25 2010 +0200
    43.3 @@ -169,7 +169,7 @@
    43.4  
    43.5      (* register constant definitions *)
    43.6      val (fixdef_thms, thy) =
    43.7 -      (PureThy.add_defs false o map Thm.no_attributes)
    43.8 +      (Global_Theory.add_defs false o map Thm.no_attributes)
    43.9          (map (Binding.suffix_name "_def") binds ~~ eqns) thy;
   43.10  
   43.11      (* prove applied version of definitions *)
   43.12 @@ -201,7 +201,7 @@
   43.13  
   43.14      (* register unfold theorems *)
   43.15      val (unfold_thms, thy) =
   43.16 -      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   43.17 +      (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   43.18          (mk_unfold_thms unfold_binds tuple_unfold_thm) thy;
   43.19    in
   43.20      ((proj_thms, unfold_thms), thy)
   43.21 @@ -242,13 +242,13 @@
   43.22      val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy;
   43.23      val eqn = Logic.mk_equals (const, rhs);
   43.24      val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn);
   43.25 -    val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy;
   43.26 +    val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy;
   43.27    in
   43.28      ((const, def_thm), thy)
   43.29    end;
   43.30  
   43.31  fun add_qualified_thm name (dbind, thm) =
   43.32 -    yield_singleton PureThy.add_thms
   43.33 +    yield_singleton Global_Theory.add_thms
   43.34        ((Binding.qualified true name dbind, thm), []);
   43.35  
   43.36  (******************************************************************************)
   43.37 @@ -349,7 +349,7 @@
   43.38      val deflation_map_binds = dbinds |>
   43.39          map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map");
   43.40      val (deflation_map_thms, thy) = thy |>
   43.41 -      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   43.42 +      (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   43.43          (conjuncts deflation_map_binds deflation_map_thm);
   43.44  
   43.45      (* register map functions in theory data *)
   43.46 @@ -496,7 +496,7 @@
   43.47      (* register REP equations *)
   43.48      val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dbinds;
   43.49      val (_, thy) = thy |>
   43.50 -      (PureThy.add_thms o map Thm.no_attributes)
   43.51 +      (Global_Theory.add_thms o map Thm.no_attributes)
   43.52          (REP_eq_binds ~~ REP_eq_thms);
   43.53  
   43.54      (* define rep/abs functions *)
   43.55 @@ -607,7 +607,7 @@
   43.56            val thmR = thm RS @{thm conjunct2};
   43.57          in (n, thmL):: conjuncts ns thmR end;
   43.58      val (isodefl_thms, thy) = thy |>
   43.59 -      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   43.60 +      (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   43.61          (conjuncts isodefl_binds isodefl_thm);
   43.62      val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
   43.63  
   43.64 @@ -631,7 +631,7 @@
   43.65        map prove_map_ID_thm
   43.66          (map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms);
   43.67      val (_, thy) = thy |>
   43.68 -      (PureThy.add_thms o map Thm.no_attributes)
   43.69 +      (Global_Theory.add_thms o map Thm.no_attributes)
   43.70          (map_ID_binds ~~ map_ID_thms);
   43.71      val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy;
   43.72  
    44.1 --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Sep 20 15:29:53 2010 +0200
    44.2 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Sep 20 16:05:25 2010 +0200
    44.3 @@ -204,15 +204,15 @@
    44.4  (******************************************************************************)
    44.5  
    44.6  fun add_qualified_def name (dbind, eqn) =
    44.7 -    yield_singleton (PureThy.add_defs false)
    44.8 +    yield_singleton (Global_Theory.add_defs false)
    44.9       ((Binding.qualified true name dbind, eqn), []);
   44.10  
   44.11  fun add_qualified_thm name (dbind, thm) =
   44.12 -    yield_singleton PureThy.add_thms
   44.13 +    yield_singleton Global_Theory.add_thms
   44.14        ((Binding.qualified true name dbind, thm), []);
   44.15  
   44.16  fun add_qualified_simp_thm name (dbind, thm) =
   44.17 -    yield_singleton PureThy.add_thms
   44.18 +    yield_singleton Global_Theory.add_thms
   44.19        ((Binding.qualified true name dbind, thm), [Simplifier.simp_add]);
   44.20  
   44.21  (******************************************************************************)
    45.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Sep 20 15:29:53 2010 +0200
    45.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Sep 20 16:05:25 2010 +0200
    45.3 @@ -124,7 +124,7 @@
    45.4  val rep_const = #rep_const iso_info;
    45.5  
    45.6  local
    45.7 -  fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
    45.8 +  fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
    45.9  in
   45.10    val ax_take_0      = ga "take_0" dname;
   45.11    val ax_take_strict = ga "take_strict" dname;
   45.12 @@ -200,7 +200,7 @@
   45.13  
   45.14  in
   45.15    thy
   45.16 -  |> PureThy.add_thmss [
   45.17 +  |> Global_Theory.add_thmss [
   45.18       ((qualified "iso_rews"  , iso_rews    ), [simp]),
   45.19       ((qualified "nchotomy"  , [nchotomy]  ), []),
   45.20       ((qualified "exhaust"   , [exhaust]   ),
   45.21 @@ -240,8 +240,8 @@
   45.22    val pg = pg' thy;
   45.23  
   45.24    local
   45.25 -    fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
   45.26 -    fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
   45.27 +    fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
   45.28 +    fun gts s dn = Global_Theory.get_thms thy (dn ^ "." ^ s);
   45.29    in
   45.30      val axs_rep_iso = map (ga "rep_iso") dnames;
   45.31      val axs_abs_iso = map (ga "abs_iso") dnames;
   45.32 @@ -421,10 +421,10 @@
   45.33  
   45.34  in
   45.35    thy
   45.36 -  |> snd o PureThy.add_thmss [
   45.37 +  |> snd o Global_Theory.add_thmss [
   45.38       ((Binding.qualified true "finite_induct" comp_dbind, [finite_ind]), []),
   45.39       ((Binding.qualified true "induct"        comp_dbind, [ind]       ), [])]
   45.40 -  |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
   45.41 +  |> (snd o Global_Theory.add_thmss (map ind_rule (dnames ~~ inducts)))
   45.42  end; (* prove_induction *)
   45.43  
   45.44  (******************************************************************************)
   45.45 @@ -444,7 +444,7 @@
   45.46  val n_eqs = length eqs;
   45.47  
   45.48  val take_rews =
   45.49 -    maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
   45.50 +    maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
   45.51  
   45.52  (* ----- define bisimulation predicate -------------------------------------- *)
   45.53  
   45.54 @@ -465,7 +465,7 @@
   45.55        singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
   45.56    fun legacy_infer_prop thy t = legacy_infer_term thy (Type.constraint propT t);
   45.57    fun infer_props thy = map (apsnd (legacy_infer_prop thy));
   45.58 -  fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
   45.59 +  fun add_defs_i x = Global_Theory.add_defs false (map Thm.no_attributes x);
   45.60    fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
   45.61  
   45.62    fun one_con (con, args) =
   45.63 @@ -568,7 +568,7 @@
   45.64      in pg [] goal (K tacs) end;
   45.65  end; (* local *)
   45.66  
   45.67 -in thy |> snd o PureThy.add_thmss
   45.68 +in thy |> snd o Global_Theory.add_thmss
   45.69      [((Binding.qualified true "coinduct" comp_dbind, [coind]), [])]
   45.70  end; (* let *)
   45.71  
   45.72 @@ -603,7 +603,7 @@
   45.73  val take_lemmas = #take_lemma_thms take_info;
   45.74  
   45.75  val take_rews =
   45.76 -    maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
   45.77 +    maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
   45.78  
   45.79  (* prove induction rules, unless definition is indirect recursive *)
   45.80  val thy =
    46.1 --- a/src/HOLCF/Tools/fixrec.ML	Mon Sep 20 15:29:53 2010 +0200
    46.2 +++ b/src/HOLCF/Tools/fixrec.ML	Mon Sep 20 16:05:25 2010 +0200
    46.3 @@ -419,7 +419,7 @@
    46.4      val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
    46.5      val cname = case chead_of t of Const(c,_) => c | _ =>
    46.6                fixrec_err "function is not declared as constant in theory";
    46.7 -    val unfold_thm = PureThy.get_thm thy (cname^".unfold");
    46.8 +    val unfold_thm = Global_Theory.get_thm thy (cname^".unfold");
    46.9      val simp = Goal.prove_global thy [] [] eq
   46.10            (fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]);
   46.11    in simp end;
   46.12 @@ -431,7 +431,7 @@
   46.13      val ts = map (prep_term thy) strings;
   46.14      val simps = map (fix_pat thy) ts;
   46.15    in
   46.16 -    (snd o PureThy.add_thmss [((name, simps), atts)]) thy
   46.17 +    (snd o Global_Theory.add_thmss [((name, simps), atts)]) thy
   46.18    end;
   46.19  
   46.20  val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
    47.1 --- a/src/HOLCF/Tools/pcpodef.ML	Mon Sep 20 15:29:53 2010 +0200
    47.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Mon Sep 20 16:05:25 2010 +0200
    47.3 @@ -100,7 +100,7 @@
    47.4      val (_, thy) =
    47.5        thy
    47.6        |> Sign.add_path (Binding.name_of name)
    47.7 -      |> PureThy.add_thms
    47.8 +      |> Global_Theory.add_thms
    47.9          ([((Binding.prefix_name "adm_"      name, admissible'), []),
   47.10            ((Binding.prefix_name "cont_" Rep_name, cont_Rep   ), []),
   47.11            ((Binding.prefix_name "cont_" Abs_name, cont_Abs   ), []),
   47.12 @@ -143,7 +143,7 @@
   47.13      val (_, thy) =
   47.14        thy
   47.15        |> Sign.add_path (Binding.name_of name)
   47.16 -      |> PureThy.add_thms
   47.17 +      |> Global_Theory.add_thms
   47.18          ([((Binding.suffix_name "_strict"     Rep_name, Rep_strict), []),
   47.19            ((Binding.suffix_name "_strict"     Abs_name, Abs_strict), []),
   47.20            ((Binding.suffix_name "_strict_iff" Rep_name, Rep_strict_iff), []),
    48.1 --- a/src/HOLCF/Tools/repdef.ML	Mon Sep 20 15:29:53 2010 +0200
    48.2 +++ b/src/HOLCF/Tools/repdef.ML	Mon Sep 20 16:05:25 2010 +0200
    48.3 @@ -139,7 +139,7 @@
    48.4        [type_definition_thm, #below_def cpo_info, emb_def, prj_def];
    48.5      val (REP_thm, thy) = thy
    48.6        |> Sign.add_path (Binding.name_of name)
    48.7 -      |> PureThy.add_thm
    48.8 +      |> Global_Theory.add_thm
    48.9           ((Binding.prefix_name "REP_" name,
   48.10            Drule.zero_var_indexes (@{thm typedef_REP} OF typedef_thms')), [])
   48.11        ||> Sign.restore_naming thy;
    49.1 --- a/src/HOLCF/ex/Pattern_Match.thy	Mon Sep 20 15:29:53 2010 +0200
    49.2 +++ b/src/HOLCF/ex/Pattern_Match.thy	Mon Sep 20 16:05:25 2010 +0200
    49.3 @@ -379,7 +379,7 @@
    49.4        (Binding.suffix_name "_def" b, Logic.mk_equals (c, t));
    49.5      val defs = map2 mk_def consts specs;
    49.6      val (def_thms, thy) =
    49.7 -      PureThy.add_defs false (map Thm.no_attributes defs) thy;
    49.8 +      Global_Theory.add_defs false (map Thm.no_attributes defs) thy;
    49.9    in
   49.10      ((consts, def_thms), thy)
   49.11    end;
    50.1 --- a/src/Pure/IsaMakefile	Mon Sep 20 15:29:53 2010 +0200
    50.2 +++ b/src/Pure/IsaMakefile	Mon Sep 20 16:05:25 2010 +0200
    50.3 @@ -218,6 +218,7 @@
    50.4    drule.ML						\
    50.5    envir.ML						\
    50.6    facts.ML						\
    50.7 +  global_theory.ML					\
    50.8    goal.ML						\
    50.9    goal_display.ML					\
   50.10    interpretation.ML					\
    51.1 --- a/src/Pure/Isar/attrib.ML	Mon Sep 20 15:29:53 2010 +0200
    51.2 +++ b/src/Pure/Isar/attrib.ML	Mon Sep 20 16:05:25 2010 +0200
    51.3 @@ -181,7 +181,7 @@
    51.4  fun gen_thm pick = Scan.depend (fn context =>
    51.5    let
    51.6      val thy = Context.theory_of context;
    51.7 -    val get = Context.cases (PureThy.get_fact context) ProofContext.get_fact context;
    51.8 +    val get = Context.cases (Global_Theory.get_fact context) ProofContext.get_fact context;
    51.9      val get_fact = get o Facts.Fact;
   51.10      fun get_named pos name = get (Facts.Named ((name, pos), NONE));
   51.11    in
    52.1 --- a/src/Pure/Isar/calculation.ML	Mon Sep 20 15:29:53 2010 +0200
    52.2 +++ b/src/Pure/Isar/calculation.ML	Mon Sep 20 16:05:25 2010 +0200
    52.3 @@ -98,7 +98,7 @@
    52.4      "declaration of symmetry rule" #>
    52.5    Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
    52.6      "resolution with symmetry rule" #>
    52.7 -  PureThy.add_thms
    52.8 +  Global_Theory.add_thms
    52.9     [((Binding.empty, transitive_thm), [trans_add]),
   52.10      ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
   52.11  
    53.1 --- a/src/Pure/Isar/class.ML	Mon Sep 20 15:29:53 2010 +0200
    53.2 +++ b/src/Pure/Isar/class.ML	Mon Sep 20 16:05:25 2010 +0200
    53.3 @@ -329,7 +329,7 @@
    53.4      |> snd
    53.5      |> Thm.add_def false false (b_def, def_eq)
    53.6      |>> apsnd Thm.varifyT_global
    53.7 -    |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm)
    53.8 +    |-> (fn (_, def_thm) => Global_Theory.store_thm (b_def, def_thm)
    53.9        #> snd
   53.10        #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
   53.11      |> Sign.add_const_constraint (c', SOME ty')
    54.1 --- a/src/Pure/Isar/context_rules.ML	Mon Sep 20 15:29:53 2010 +0200
    54.2 +++ b/src/Pure/Isar/context_rules.ML	Mon Sep 20 16:05:25 2010 +0200
    54.3 @@ -196,7 +196,7 @@
    54.4  val dest_query  = rule_add elim_queryK Tactic.make_elim;
    54.5  
    54.6  val _ = Context.>> (Context.map_theory
    54.7 -  (snd o PureThy.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]));
    54.8 +  (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]));
    54.9  
   54.10  
   54.11  (* concrete syntax *)
    55.1 --- a/src/Pure/Isar/element.ML	Mon Sep 20 15:29:53 2010 +0200
    55.2 +++ b/src/Pure/Isar/element.ML	Mon Sep 20 16:05:25 2010 +0200
    55.3 @@ -480,7 +480,7 @@
    55.4      val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
    55.5    in
    55.6      context |> Context.mapping_result
    55.7 -      (PureThy.note_thmss kind facts')
    55.8 +      (Global_Theory.note_thmss kind facts')
    55.9        (ProofContext.note_thmss kind facts')
   55.10    end;
   55.11  
    56.1 --- a/src/Pure/Isar/expression.ML	Mon Sep 20 15:29:53 2010 +0200
    56.2 +++ b/src/Pure/Isar/expression.ML	Mon Sep 20 16:05:25 2010 +0200
    56.3 @@ -640,7 +640,7 @@
    56.4        thy
    56.5        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
    56.6        |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
    56.7 -      |> PureThy.add_defs false
    56.8 +      |> Global_Theory.add_defs false
    56.9          [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
   56.10      val defs_ctxt = ProofContext.init_global defs_thy |> Variable.declare_term head;
   56.11  
   56.12 @@ -681,7 +681,7 @@
   56.13            val (_, thy'') =
   56.14              thy'
   56.15              |> Sign.qualified_path true abinding
   56.16 -            |> PureThy.note_thmss ""
   56.17 +            |> Global_Theory.note_thmss ""
   56.18                [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
   56.19              ||> Sign.restore_naming thy';
   56.20            in (SOME statement, SOME intro, axioms, thy'') end;
   56.21 @@ -695,7 +695,7 @@
   56.22            val (_, thy'''') =
   56.23              thy'''
   56.24              |> Sign.qualified_path true binding
   56.25 -            |> PureThy.note_thmss ""
   56.26 +            |> Global_Theory.note_thmss ""
   56.27                   [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
   56.28                    ((Binding.conceal (Binding.name axiomsN), []),
   56.29                      [(map (Drule.export_without_context o Element.conclude_witness) axioms, [])])]
    57.1 --- a/src/Pure/Isar/generic_target.ML	Mon Sep 20 15:29:53 2010 +0200
    57.2 +++ b/src/Pure/Isar/generic_target.ML	Mon Sep 20 16:05:25 2010 +0200
    57.3 @@ -122,7 +122,7 @@
    57.4        |> Drule.zero_var_indexes_list;
    57.5  
    57.6      (*thm definition*)
    57.7 -    val result = PureThy.name_thm true true name th'';
    57.8 +    val result = Global_Theory.name_thm true true name th'';
    57.9  
   57.10      (*import fixes*)
   57.11      val (tvars, vars) =
   57.12 @@ -142,7 +142,7 @@
   57.13          NONE => raise THM ("Failed to re-import result", 0, [result'])
   57.14        | SOME res => Local_Defs.contract ctxt defs (Thm.cprop_of th) res)
   57.15        |> Goal.norm_result
   57.16 -      |> PureThy.name_thm false false name;
   57.17 +      |> Global_Theory.name_thm false false name;
   57.18  
   57.19    in (result'', result) end;
   57.20  
   57.21 @@ -150,11 +150,11 @@
   57.22    let
   57.23      val thy = ProofContext.theory_of lthy;
   57.24      val facts' = facts
   57.25 -      |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi
   57.26 +      |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
   57.27            (Local_Theory.full_name lthy (fst a))) bs))
   57.28 -      |> PureThy.map_facts (import_export_proof lthy);
   57.29 -    val local_facts = PureThy.map_facts #1 facts';
   57.30 -    val global_facts = PureThy.map_facts #2 facts';
   57.31 +      |> Global_Theory.map_facts (import_export_proof lthy);
   57.32 +    val local_facts = Global_Theory.map_facts #1 facts';
   57.33 +    val global_facts = Global_Theory.map_facts #2 facts';
   57.34    in
   57.35      lthy
   57.36      |> target_notes kind global_facts local_facts
   57.37 @@ -214,7 +214,7 @@
   57.38      val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
   57.39    in
   57.40      lthy
   57.41 -    |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
   57.42 +    |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
   57.43      |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
   57.44    end;
   57.45  
    58.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Sep 20 15:29:53 2010 +0200
    58.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Sep 20 16:05:25 2010 +0200
    58.3 @@ -174,8 +174,9 @@
    58.4  val add_axioms = fold (snd oo Specification.axiom_cmd);
    58.5  
    58.6  fun add_defs ((unchecked, overloaded), args) thy =
    58.7 -  thy |> (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded
    58.8 -    (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args)
    58.9 +  thy |>
   58.10 +    (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
   58.11 +      overloaded (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args)
   58.12    |> snd;
   58.13  
   58.14  
   58.15 @@ -215,7 +216,8 @@
   58.16  val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class;
   58.17  val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type;
   58.18  val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const;
   58.19 -val hide_fact = hide_names PureThy.intern_fact PureThy.defined_fact PureThy.hide_fact;
   58.20 +val hide_fact =
   58.21 +  hide_names Global_Theory.intern_fact Global_Theory.defined_fact Global_Theory.hide_fact;
   58.22  
   58.23  
   58.24  (* goals *)
    59.1 --- a/src/Pure/Isar/locale.ML	Mon Sep 20 15:29:53 2010 +0200
    59.2 +++ b/src/Pure/Isar/locale.ML	Mon Sep 20 16:05:25 2010 +0200
    59.3 @@ -506,7 +506,7 @@
    59.4              let
    59.5                val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
    59.6                  Attrib.map_facts (Attrib.attribute_i thy)
    59.7 -            in PureThy.note_thmss kind args'' #> snd end)
    59.8 +            in Global_Theory.note_thmss kind args'' #> snd end)
    59.9          (registrations_of (Context.Theory thy) loc) thy))
   59.10    in ctxt'' end;
   59.11  
    60.1 --- a/src/Pure/Isar/named_target.ML	Mon Sep 20 15:29:53 2010 +0200
    60.2 +++ b/src/Pure/Isar/named_target.ML	Mon Sep 20 16:05:25 2010 +0200
    60.3 @@ -118,7 +118,7 @@
    60.4        (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
    60.5    in
    60.6      lthy
    60.7 -    |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
    60.8 +    |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
    60.9      |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
   60.10    end
   60.11  
    61.1 --- a/src/Pure/Isar/proof_context.ML	Mon Sep 20 15:29:53 2010 +0200
    61.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Sep 20 16:05:25 2010 +0200
    61.3 @@ -297,7 +297,7 @@
    61.4  fun extern_fact ctxt name =
    61.5    let
    61.6      val local_facts = facts_of ctxt;
    61.7 -    val global_facts = PureThy.facts_of (theory_of ctxt);
    61.8 +    val global_facts = Global_Theory.facts_of (theory_of ctxt);
    61.9    in
   61.10      if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
   61.11      then Facts.extern local_facts name
   61.12 @@ -790,7 +790,7 @@
   61.13        extern_const = Consts.extern consts};
   61.14    in
   61.15      Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
   61.16 -      (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax (theory_of ctxt)))
   61.17 +      (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (theory_of ctxt)))
   61.18    end;
   61.19  
   61.20  in
   61.21 @@ -982,7 +982,7 @@
   61.22                SOME (_, ths) =>
   61.23                 (Context_Position.report ctxt pos (Markup.local_fact name);
   61.24                  map (Thm.transfer thy) (Facts.select thmref ths))
   61.25 -            | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
   61.26 +            | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
   61.27        in pick name thms end;
   61.28  
   61.29  in
   61.30 @@ -1012,12 +1012,12 @@
   61.31      val name = full_name ctxt b;
   61.32      val _ = Context_Position.report ctxt pos (Markup.local_fact_decl name);
   61.33  
   61.34 -    val facts = PureThy.name_thmss false name raw_facts;
   61.35 +    val facts = Global_Theory.name_thmss false name raw_facts;
   61.36      fun app (th, attrs) x =
   61.37        swap (Library.foldl_map
   61.38          (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
   61.39      val (res, ctxt') = fold_map app facts ctxt;
   61.40 -    val thms = PureThy.name_thms false false name (flat res);
   61.41 +    val thms = Global_Theory.name_thms false false name (flat res);
   61.42      val Mode {stmt, ...} = get_mode ctxt;
   61.43    in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
   61.44  
    62.1 --- a/src/Pure/Isar/proof_display.ML	Mon Sep 20 15:29:53 2010 +0200
    62.2 +++ b/src/Pure/Isar/proof_display.ML	Mon Sep 20 16:05:25 2010 +0200
    62.3 @@ -49,9 +49,9 @@
    62.4  fun pretty_theorems_diff verbose prev_thys thy =
    62.5    let
    62.6      val pretty_fact = ProofContext.pretty_fact (ProofContext.init_global thy);
    62.7 -    val facts = PureThy.facts_of thy;
    62.8 +    val facts = Global_Theory.facts_of thy;
    62.9      val thmss =
   62.10 -      Facts.dest_static (map PureThy.facts_of prev_thys) facts
   62.11 +      Facts.dest_static (map Global_Theory.facts_of prev_thys) facts
   62.12        |> not verbose ? filter_out (Facts.is_concealed facts o #1);
   62.13    in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
   62.14  
    63.1 --- a/src/Pure/Isar/specification.ML	Mon Sep 20 15:29:53 2010 +0200
    63.2 +++ b/src/Pure/Isar/specification.ML	Mon Sep 20 16:05:25 2010 +0200
    63.3 @@ -180,7 +180,7 @@
    63.4      val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
    63.5          fold_map Thm.add_axiom
    63.6            (map (apfst (fn a => Binding.map_name (K a) b))
    63.7 -            (PureThy.name_multi (Name.of_binding b) (map subst props)))
    63.8 +            (Global_Theory.name_multi (Name.of_binding b) (map subst props)))
    63.9          #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
   63.10  
   63.11      (*facts*)
    64.1 --- a/src/Pure/ML/ml_context.ML	Mon Sep 20 15:29:53 2010 +0200
    64.2 +++ b/src/Pure/ML/ml_context.ML	Mon Sep 20 16:05:25 2010 +0200
    64.3 @@ -75,7 +75,7 @@
    64.4  fun ml_store get (name, ths) =
    64.5    let
    64.6      val ths' = Context.>>> (Context.map_theory_result
    64.7 -      (PureThy.store_thms (Binding.name name, ths)));
    64.8 +      (Global_Theory.store_thms (Binding.name name, ths)));
    64.9      val _ = Context.>> (Context.map_theory (Stored_Thms.put ths'));
   64.10      val _ =
   64.11        if name = "" then ()
    65.1 --- a/src/Pure/Proof/extraction.ML	Mon Sep 20 15:29:53 2010 +0200
    65.2 +++ b/src/Pure/Proof/extraction.ML	Mon Sep 20 16:05:25 2010 +0200
    65.3 @@ -783,11 +783,11 @@
    65.4               val (def_thms, thy') = if t = nullt then ([], thy) else
    65.5                 thy
    65.6                 |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
    65.7 -               |> PureThy.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"),
    65.8 +               |> Global_Theory.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"),
    65.9                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
   65.10             in
   65.11               thy'
   65.12 -             |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
   65.13 +             |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
   65.14                    Thm.varifyT_global (funpow (length (vars_of corr_prop))
   65.15                      (Thm.forall_elim_var 0) (Thm.forall_intr_frees
   65.16                        (ProofChecker.thm_of_proof thy'
   65.17 @@ -815,7 +815,7 @@
   65.18    Keyword.thy_decl
   65.19      (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
   65.20       (fn xs => Toplevel.theory (fn thy => add_realizers
   65.21 -       (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
   65.22 +       (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
   65.23  
   65.24  val _ =
   65.25    Outer_Syntax.command "realizability"
   65.26 @@ -830,7 +830,7 @@
   65.27  val _ =
   65.28    Outer_Syntax.command "extract" "extract terms from proofs" Keyword.thy_decl
   65.29      (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
   65.30 -      extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
   65.31 +      extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
   65.32  
   65.33  val etype_of = etype_of o add_syntax;
   65.34  
    66.1 --- a/src/Pure/Proof/proof_syntax.ML	Mon Sep 20 15:29:53 2010 +0200
    66.2 +++ b/src/Pure/Proof/proof_syntax.ML	Mon Sep 20 16:05:25 2010 +0200
    66.3 @@ -88,7 +88,7 @@
    66.4  
    66.5  fun proof_of_term thy ty =
    66.6    let
    66.7 -    val thms = PureThy.all_thms_of thy;
    66.8 +    val thms = Global_Theory.all_thms_of thy;
    66.9      val axms = Theory.all_axioms_of thy;
   66.10  
   66.11      fun mk_term t = (if ty then I else map_types (K dummyT))
   66.12 @@ -188,7 +188,7 @@
   66.13  
   66.14  fun cterm_of_proof thy prf =
   66.15    let
   66.16 -    val thm_names = map fst (PureThy.all_thms_of thy);
   66.17 +    val thm_names = map fst (Global_Theory.all_thms_of thy);
   66.18      val axm_names = map fst (Theory.all_axioms_of thy);
   66.19      val thy' = thy
   66.20        |> add_proof_syntax
   66.21 @@ -207,7 +207,7 @@
   66.22  
   66.23  fun read_term thy topsort =
   66.24    let
   66.25 -    val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy));
   66.26 +    val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy));
   66.27      val axm_names = map fst (Theory.all_axioms_of thy);
   66.28      val ctxt = thy
   66.29        |> add_proof_syntax
    67.1 --- a/src/Pure/Proof/proofchecker.ML	Mon Sep 20 15:29:53 2010 +0200
    67.2 +++ b/src/Pure/Proof/proofchecker.ML	Mon Sep 20 16:05:25 2010 +0200
    67.3 @@ -16,7 +16,7 @@
    67.4  (***** construct a theorem out of a proof term *****)
    67.5  
    67.6  fun lookup_thm thy =
    67.7 -  let val tab = fold_rev Symtab.update (PureThy.all_thms_of thy) Symtab.empty
    67.8 +  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty
    67.9    in
   67.10      (fn s => case Symtab.lookup tab s of
   67.11         NONE => error ("Unknown theorem " ^ quote s)
    68.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 20 15:29:53 2010 +0200
    68.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 20 16:05:25 2010 +0200
    68.3 @@ -267,8 +267,8 @@
    68.4  
    68.5  fun new_thms_deps thy thy' =
    68.6    let
    68.7 -    val prev_facts = PureThy.facts_of thy;
    68.8 -    val facts = PureThy.facts_of thy';
    68.9 +    val prev_facts = Global_Theory.facts_of thy;
   68.10 +    val facts = Global_Theory.facts_of thy';
   68.11    in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end;
   68.12  
   68.13  end;
   68.14 @@ -519,7 +519,7 @@
   68.15  
   68.16  fun theory_facts name =
   68.17    let val thy = Thy_Info.get_theory name
   68.18 -  in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end;
   68.19 +  in (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy) end;
   68.20  
   68.21  fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
   68.22  fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static);
   68.23 @@ -608,7 +608,7 @@
   68.24                     What we want is mapping onto simple PGIP name/context model. *)
   68.25                  val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
   68.26                  val thy = ProofContext.theory_of ctx
   68.27 -                val ths = [PureThy.get_thm thy thmname]
   68.28 +                val ths = [Global_Theory.get_thm thy thmname]
   68.29                  val deps = #2 (thms_deps ths);
   68.30              in
   68.31                  if null deps then ()
   68.32 @@ -649,7 +649,7 @@
   68.33                                    text=[XML.Elem (("pgml", []), maps YXML.parse_body strings)] })
   68.34  
   68.35          fun strings_of_thm (thy, name) =
   68.36 -          map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
   68.37 +          map (Display.string_of_thm_global thy) (Global_Theory.get_thms thy name)
   68.38  
   68.39          val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
   68.40      in
    69.1 --- a/src/Pure/ROOT.ML	Mon Sep 20 15:29:53 2010 +0200
    69.2 +++ b/src/Pure/ROOT.ML	Mon Sep 20 16:05:25 2010 +0200
    69.3 @@ -134,6 +134,7 @@
    69.4  use "thm.ML";
    69.5  use "more_thm.ML";
    69.6  use "facts.ML";
    69.7 +use "global_theory.ML";
    69.8  use "pure_thy.ML";
    69.9  use "drule.ML";
   69.10  use "morphism.ML";
    70.1 --- a/src/Pure/Thy/thm_deps.ML	Mon Sep 20 15:29:53 2010 +0200
    70.2 +++ b/src/Pure/Thy/thm_deps.ML	Mon Sep 20 16:05:25 2010 +0200
    70.3 @@ -49,7 +49,7 @@
    70.4  fun unused_thms (base_thys, thys) =
    70.5    let
    70.6      fun add_fact space (name, ths) =
    70.7 -      if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
    70.8 +      if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
    70.9        else
   70.10          let val {concealed, group, ...} = Name_Space.the_entry space name in
   70.11            fold_rev (fn th =>
   70.12 @@ -60,7 +60,7 @@
   70.13      fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
   70.14  
   70.15      val new_thms =
   70.16 -      fold (add_facts o PureThy.facts_of) thys []
   70.17 +      fold (add_facts o Global_Theory.facts_of) thys []
   70.18        |> sort_distinct (string_ord o pairself #1);
   70.19  
   70.20      val used =
    71.1 --- a/src/Pure/Thy/thy_info.ML	Mon Sep 20 15:29:53 2010 +0200
    71.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Sep 20 16:05:25 2010 +0200
    71.3 @@ -194,7 +194,7 @@
    71.4        tasks |> maps (fn name =>
    71.5          let
    71.6            val (thy, after_load) = Future.join (the (Symtab.lookup futures name));
    71.7 -          val _ = PureThy.join_proofs thy;
    71.8 +          val _ = Global_Theory.join_proofs thy;
    71.9            val _ = after_load ();
   71.10          in [] end handle exn => [Exn.Exn exn])
   71.11        |> rev |> Exn.release_all;
    72.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Sep 20 15:29:53 2010 +0200
    72.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Sep 20 16:05:25 2010 +0200
    72.3 @@ -350,7 +350,7 @@
    72.4  fun nicer_shortest ctxt =
    72.5    let
    72.6      (* FIXME global name space!? *)
    72.7 -    val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
    72.8 +    val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt));
    72.9  
   72.10      val shorten =
   72.11        Name_Space.extern_flags
   72.12 @@ -381,7 +381,7 @@
   72.13        |> filter_out (Facts.is_concealed facts o #1);
   72.14    in
   72.15      maps Facts.selections
   72.16 -     (visible_facts (PureThy.facts_of (ProofContext.theory_of ctxt)) @
   72.17 +     (visible_facts (Global_Theory.facts_of (ProofContext.theory_of ctxt)) @
   72.18        visible_facts (ProofContext.facts_of ctxt))
   72.19    end;
   72.20  
    73.1 --- a/src/Pure/Tools/named_thms.ML	Mon Sep 20 15:29:53 2010 +0200
    73.2 +++ b/src/Pure/Tools/named_thms.ML	Mon Sep 20 16:05:25 2010 +0200
    73.3 @@ -39,6 +39,6 @@
    73.4  
    73.5  val setup =
    73.6    Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
    73.7 -  PureThy.add_thms_dynamic (Binding.name name, content);
    73.8 +  Global_Theory.add_thms_dynamic (Binding.name name, content);
    73.9  
   73.10  end;
    74.1 --- a/src/Pure/assumption.ML	Mon Sep 20 15:29:53 2010 +0200
    74.2 +++ b/src/Pure/assumption.ML	Mon Sep 20 16:05:25 2010 +0200
    74.3 @@ -81,7 +81,7 @@
    74.4  
    74.5  (*named prems -- legacy feature*)
    74.6  val _ = Context.>>
    74.7 -  (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
    74.8 +  (Context.map_theory (Global_Theory.add_thms_dynamic (Binding.name "prems",
    74.9      fn Context.Theory _ => [] | Context.Proof ctxt => all_prems_of ctxt)));
   74.10  
   74.11  
    75.1 --- a/src/Pure/axclass.ML	Mon Sep 20 15:29:53 2010 +0200
    75.2 +++ b/src/Pure/axclass.ML	Mon Sep 20 16:05:25 2010 +0200
    75.3 @@ -390,7 +390,7 @@
    75.4          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
    75.5        #>> apsnd Thm.varifyT_global
    75.6        #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
    75.7 -        #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
    75.8 +        #> Global_Theory.add_thm ((Binding.conceal (Binding.name c'), thm), [])
    75.9          #> #2
   75.10          #> pair (Const (c, T))))
   75.11      ||> Sign.restore_naming thy
   75.12 @@ -419,7 +419,7 @@
   75.13      fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
   75.14      val rel = Logic.dest_classrel prop handle TERM _ => err ();
   75.15      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
   75.16 -    val (th', thy') = PureThy.store_thm
   75.17 +    val (th', thy') = Global_Theory.store_thm
   75.18        (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
   75.19      val th'' = th'
   75.20        |> Thm.unconstrainT
   75.21 @@ -438,7 +438,7 @@
   75.22      fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
   75.23      val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
   75.24  
   75.25 -    val (th', thy') = PureThy.store_thm
   75.26 +    val (th', thy') = Global_Theory.store_thm
   75.27        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
   75.28  
   75.29      val args = Name.names Name.context Name.aT Ss;
   75.30 @@ -560,7 +560,7 @@
   75.31      val ([def], def_thy) =
   75.32        thy
   75.33        |> Sign.primitive_class (bclass, super)
   75.34 -      |> PureThy.add_defs false [((Thm.def_binding bconst, class_eq), [])];
   75.35 +      |> Global_Theory.add_defs false [((Thm.def_binding bconst, class_eq), [])];
   75.36      val (raw_intro, (raw_classrel, raw_axioms)) =
   75.37        split_defined (length conjs) def ||> chop (length super);
   75.38  
   75.39 @@ -571,7 +571,7 @@
   75.40      val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
   75.41        def_thy
   75.42        |> Sign.qualified_path true bconst
   75.43 -      |> PureThy.note_thmss ""
   75.44 +      |> Global_Theory.note_thmss ""
   75.45          [((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]),
   75.46           ((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]),
   75.47           ((Binding.name "axioms", []),
   75.48 @@ -586,7 +586,8 @@
   75.49        facts_thy
   75.50        |> fold (#2 oo put_trancl_classrel) (map (pair class) super ~~ classrel)
   75.51        |> Sign.qualified_path false bconst
   75.52 -      |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> #2
   75.53 +      |> Global_Theory.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms))
   75.54 +      |> #2
   75.55        |> Sign.restore_naming facts_thy
   75.56        |> map_axclasses (Symtab.update (class, axclass))
   75.57        |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
    76.1 --- a/src/Pure/drule.ML	Mon Sep 20 15:29:53 2010 +0200
    76.2 +++ b/src/Pure/drule.ML	Mon Sep 20 16:05:25 2010 +0200
    76.3 @@ -433,10 +433,10 @@
    76.4  val read_prop = certify o Simple_Syntax.read_prop;
    76.5  
    76.6  fun store_thm name th =
    76.7 -  Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
    76.8 +  Context.>>> (Context.map_theory_result (Global_Theory.store_thm (name, th)));
    76.9  
   76.10  fun store_thm_open name th =
   76.11 -  Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
   76.12 +  Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th)));
   76.13  
   76.14  fun store_standard_thm name th = store_thm name (export_without_context th);
   76.15  fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm);
    77.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    77.2 +++ b/src/Pure/global_theory.ML	Mon Sep 20 16:05:25 2010 +0200
    77.3 @@ -0,0 +1,224 @@
    77.4 +(*  Title:      Pure/global_theory.ML
    77.5 +    Author:     Makarius
    77.6 +
    77.7 +Global theory content: stored facts.
    77.8 +*)
    77.9 +
   77.10 +signature GLOBAL_THEORY =
   77.11 +sig
   77.12 +  val facts_of: theory -> Facts.T
   77.13 +  val intern_fact: theory -> xstring -> string
   77.14 +  val defined_fact: theory -> string -> bool
   77.15 +  val hide_fact: bool -> string -> theory -> theory
   77.16 +  val join_proofs: theory -> unit
   77.17 +  val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   77.18 +  val get_thms: theory -> xstring -> thm list
   77.19 +  val get_thm: theory -> xstring -> thm
   77.20 +  val all_thms_of: theory -> (string * thm) list
   77.21 +  val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   77.22 +  val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
   77.23 +  val burrow_facts: ('a list -> 'b list) ->
   77.24 +    ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   77.25 +  val name_multi: string -> 'a list -> (string * 'a) list
   77.26 +  val name_thm: bool -> bool -> string -> thm -> thm
   77.27 +  val name_thms: bool -> bool -> string -> thm list -> thm list
   77.28 +  val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
   77.29 +  val store_thms: binding * thm list -> theory -> thm list * theory
   77.30 +  val store_thm: binding * thm -> theory -> thm * theory
   77.31 +  val store_thm_open: binding * thm -> theory -> thm * theory
   77.32 +  val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
   77.33 +  val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
   77.34 +  val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
   77.35 +  val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
   77.36 +  val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
   77.37 +    -> theory -> (string * thm list) list * theory
   77.38 +  val add_defs: bool -> ((binding * term) * attribute list) list ->
   77.39 +    theory -> thm list * theory
   77.40 +  val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
   77.41 +    theory -> thm list * theory
   77.42 +  val add_defs_cmd: bool -> ((binding * string) * attribute list) list ->
   77.43 +    theory -> thm list * theory
   77.44 +  val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list ->
   77.45 +    theory -> thm list * theory
   77.46 +end;
   77.47 +
   77.48 +structure Global_Theory: GLOBAL_THEORY =
   77.49 +struct
   77.50 +
   77.51 +(** theory data **)
   77.52 +
   77.53 +structure Data = Theory_Data
   77.54 +(
   77.55 +  type T = Facts.T * thm list;
   77.56 +  val empty = (Facts.empty, []);
   77.57 +  fun extend (facts, _) = (facts, []);
   77.58 +  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
   77.59 +);
   77.60 +
   77.61 +
   77.62 +(* facts *)
   77.63 +
   77.64 +val facts_of = #1 o Data.get;
   77.65 +
   77.66 +val intern_fact = Facts.intern o facts_of;
   77.67 +val defined_fact = Facts.defined o facts_of;
   77.68 +
   77.69 +fun hide_fact fully name = Data.map (apfst (Facts.hide fully name));
   77.70 +
   77.71 +
   77.72 +(* proofs *)
   77.73 +
   77.74 +fun register_proofs (thy, thms) = (Data.map (apsnd (append thms)) thy, thms);
   77.75 +
   77.76 +fun join_proofs thy = Thm.join_proofs (rev (#2 (Data.get thy)));
   77.77 +
   77.78 +
   77.79 +
   77.80 +(** retrieve theorems **)
   77.81 +
   77.82 +fun get_fact context thy xthmref =
   77.83 +  let
   77.84 +    val xname = Facts.name_of_ref xthmref;
   77.85 +    val pos = Facts.pos_of_ref xthmref;
   77.86 +
   77.87 +    val name = intern_fact thy xname;
   77.88 +    val res = Facts.lookup context (facts_of thy) name;
   77.89 +    val _ = Theory.check_thy thy;
   77.90 +  in
   77.91 +    (case res of
   77.92 +      NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
   77.93 +    | SOME (static, ths) =>
   77.94 +        (Position.report pos ((if static then Markup.fact else Markup.dynamic_fact) name);
   77.95 +         Facts.select xthmref (map (Thm.transfer thy) ths)))
   77.96 +  end;
   77.97 +
   77.98 +fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
   77.99 +fun get_thm thy name = Facts.the_single name (get_thms thy name);
  77.100 +
  77.101 +fun all_thms_of thy =
  77.102 +  Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
  77.103 +
  77.104 +
  77.105 +
  77.106 +(** store theorems **)
  77.107 +
  77.108 +(* fact specifications *)
  77.109 +
  77.110 +fun map_facts f = map (apsnd (map (apfst (map f))));
  77.111 +fun burrow_fact f = split_list #>> burrow f #> op ~~;
  77.112 +fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
  77.113 +
  77.114 +
  77.115 +(* naming *)
  77.116 +
  77.117 +fun name_multi name [x] = [(name, x)]
  77.118 +  | name_multi "" xs = map (pair "") xs
  77.119 +  | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
  77.120 +
  77.121 +fun name_thm pre official name thm = thm
  77.122 +  |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name
  77.123 +  |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
  77.124 +
  77.125 +fun name_thms pre official name xs =
  77.126 +  map (uncurry (name_thm pre official)) (name_multi name xs);
  77.127 +
  77.128 +fun name_thmss official name fact =
  77.129 +  burrow_fact (name_thms true official name) fact;
  77.130 +
  77.131 +
  77.132 +(* enter_thms *)
  77.133 +
  77.134 +fun enter_thms pre_name post_name app_att (b, thms) thy =
  77.135 +  if Binding.is_empty b
  77.136 +  then swap (register_proofs (app_att (thy, thms)))
  77.137 +  else
  77.138 +    let
  77.139 +      val naming = Sign.naming_of thy;
  77.140 +      val name = Name_Space.full_name naming b;
  77.141 +      val (thy', thms') =
  77.142 +        register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
  77.143 +      val thms'' = map (Thm.transfer thy') thms';
  77.144 +      val thy'' = thy' |> (Data.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
  77.145 +    in (thms'', thy'') end;
  77.146 +
  77.147 +
  77.148 +(* store_thm(s) *)
  77.149 +
  77.150 +fun store_thms (b, thms) =
  77.151 +  enter_thms (name_thms true true) (name_thms false true) I (b, thms);
  77.152 +
  77.153 +fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
  77.154 +
  77.155 +fun store_thm_open (b, th) =
  77.156 +  enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single;
  77.157 +
  77.158 +
  77.159 +(* add_thms(s) *)
  77.160 +
  77.161 +fun add_thms_atts pre_name ((b, thms), atts) =
  77.162 +  enter_thms pre_name (name_thms false true)
  77.163 +    (Library.foldl_map (Thm.theory_attributes atts)) (b, thms);
  77.164 +
  77.165 +fun gen_add_thmss pre_name =
  77.166 +  fold_map (add_thms_atts pre_name);
  77.167 +
  77.168 +fun gen_add_thms pre_name args =
  77.169 +  apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
  77.170 +
  77.171 +val add_thmss = gen_add_thmss (name_thms true true);
  77.172 +val add_thms = gen_add_thms (name_thms true true);
  77.173 +val add_thm = yield_singleton add_thms;
  77.174 +
  77.175 +
  77.176 +(* add_thms_dynamic *)
  77.177 +
  77.178 +fun add_thms_dynamic (b, f) thy = thy
  77.179 +  |> (Data.map o apfst)
  77.180 +      (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
  77.181 +
  77.182 +
  77.183 +(* note_thmss *)
  77.184 +
  77.185 +fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
  77.186 +  let
  77.187 +    val pos = Binding.pos_of b;
  77.188 +    val name = Sign.full_name thy b;
  77.189 +    val _ = Position.report pos (Markup.fact_decl name);
  77.190 +
  77.191 +    fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
  77.192 +    val (thms, thy') = thy |> enter_thms
  77.193 +      (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app)
  77.194 +      (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
  77.195 +  in ((name, thms), thy') end);
  77.196 +
  77.197 +
  77.198 +(* store axioms as theorems *)
  77.199 +
  77.200 +local
  77.201 +
  77.202 +fun no_read _ (_, t) = t;
  77.203 +
  77.204 +fun read thy (b, str) =
  77.205 +  Syntax.read_prop_global thy str handle ERROR msg =>
  77.206 +    cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
  77.207 +
  77.208 +fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
  77.209 +  let
  77.210 +    val prop = prep thy (b, raw_prop);
  77.211 +    val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
  77.212 +    val thm = def
  77.213 +      |> Thm.forall_intr_frees
  77.214 +      |> Thm.forall_elim_vars 0
  77.215 +      |> Thm.varifyT_global;
  77.216 +  in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end);
  77.217 +
  77.218 +in
  77.219 +
  77.220 +val add_defs = add no_read false;
  77.221 +val add_defs_unchecked = add no_read true;
  77.222 +val add_defs_cmd = add read false;
  77.223 +val add_defs_unchecked_cmd = add read true;
  77.224 +
  77.225 +end;
  77.226 +
  77.227 +end;
    78.1 --- a/src/Pure/pure_thy.ML	Mon Sep 20 15:29:53 2010 +0200
    78.2 +++ b/src/Pure/pure_thy.ML	Mon Sep 20 16:05:25 2010 +0200
    78.3 @@ -1,235 +1,18 @@
    78.4  (*  Title:      Pure/pure_thy.ML
    78.5      Author:     Markus Wenzel, TU Muenchen
    78.6  
    78.7 -Theorem storage.  Pure theory syntax and logical content.
    78.8 +Pure theory syntax and further logical content.
    78.9  *)
   78.10  
   78.11  signature PURE_THY =
   78.12  sig
   78.13 -  val facts_of: theory -> Facts.T
   78.14 -  val intern_fact: theory -> xstring -> string
   78.15 -  val defined_fact: theory -> string -> bool
   78.16 -  val hide_fact: bool -> string -> theory -> theory
   78.17 -  val join_proofs: theory -> unit
   78.18 -  val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   78.19 -  val get_thms: theory -> xstring -> thm list
   78.20 -  val get_thm: theory -> xstring -> thm
   78.21 -  val all_thms_of: theory -> (string * thm) list
   78.22 -  val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   78.23 -  val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
   78.24 -  val burrow_facts: ('a list -> 'b list) ->
   78.25 -    ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   78.26 -  val name_multi: string -> 'a list -> (string * 'a) list
   78.27 -  val name_thm: bool -> bool -> string -> thm -> thm
   78.28 -  val name_thms: bool -> bool -> string -> thm list -> thm list
   78.29 -  val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
   78.30 -  val store_thms: binding * thm list -> theory -> thm list * theory
   78.31 -  val store_thm: binding * thm -> theory -> thm * theory
   78.32 -  val store_thm_open: binding * thm -> theory -> thm * theory
   78.33 -  val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
   78.34 -  val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
   78.35 -  val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
   78.36 -  val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
   78.37 -  val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
   78.38 -    -> theory -> (string * thm list) list * theory
   78.39 -  val add_defs: bool -> ((binding * term) * attribute list) list ->
   78.40 -    theory -> thm list * theory
   78.41 -  val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
   78.42 -    theory -> thm list * theory
   78.43 -  val add_defs_cmd: bool -> ((binding * string) * attribute list) list ->
   78.44 -    theory -> thm list * theory
   78.45 -  val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list ->
   78.46 -    theory -> thm list * theory
   78.47    val old_appl_syntax: theory -> bool
   78.48    val old_appl_syntax_setup: theory -> theory
   78.49  end;
   78.50  
   78.51 -structure PureThy: PURE_THY =
   78.52 +structure Pure_Thy: PURE_THY =
   78.53  struct
   78.54  
   78.55 -
   78.56 -(*** stored facts ***)
   78.57 -
   78.58 -(** theory data **)
   78.59 -
   78.60 -structure Global_Facts = Theory_Data
   78.61 -(
   78.62 -  type T = Facts.T * thm list;
   78.63 -  val empty = (Facts.empty, []);
   78.64 -  fun extend (facts, _) = (facts, []);
   78.65 -  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
   78.66 -);
   78.67 -
   78.68 -
   78.69 -(* facts *)
   78.70 -
   78.71 -val facts_of = #1 o Global_Facts.get;
   78.72 -
   78.73 -val intern_fact = Facts.intern o facts_of;
   78.74 -val defined_fact = Facts.defined o facts_of;
   78.75 -
   78.76 -fun hide_fact fully name = Global_Facts.map (apfst (Facts.hide fully name));
   78.77 -
   78.78 -
   78.79 -(* proofs *)
   78.80 -
   78.81 -fun register_proofs (thy, thms) = (Global_Facts.map (apsnd (append thms)) thy, thms);
   78.82 -
   78.83 -fun join_proofs thy = Thm.join_proofs (rev (#2 (Global_Facts.get thy)));
   78.84 -
   78.85 -
   78.86 -
   78.87 -(** retrieve theorems **)
   78.88 -
   78.89 -fun get_fact context thy xthmref =
   78.90 -  let
   78.91 -    val xname = Facts.name_of_ref xthmref;
   78.92 -    val pos = Facts.pos_of_ref xthmref;
   78.93 -
   78.94 -    val name = intern_fact thy xname;
   78.95 -    val res = Facts.lookup context (facts_of thy) name;
   78.96 -    val _ = Theory.check_thy thy;
   78.97 -  in
   78.98 -    (case res of
   78.99 -      NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
  78.100 -    | SOME (static, ths) =>
  78.101 -        (Position.report pos ((if static then Markup.fact else Markup.dynamic_fact) name);
  78.102 -         Facts.select xthmref (map (Thm.transfer thy) ths)))
  78.103 -  end;
  78.104 -
  78.105 -fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
  78.106 -fun get_thm thy name = Facts.the_single name (get_thms thy name);
  78.107 -
  78.108 -fun all_thms_of thy =
  78.109 -  Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
  78.110 -
  78.111 -
  78.112 -
  78.113 -(** store theorems **)
  78.114 -
  78.115 -(* fact specifications *)
  78.116 -
  78.117 -fun map_facts f = map (apsnd (map (apfst (map f))));
  78.118 -fun burrow_fact f = split_list #>> burrow f #> op ~~;
  78.119 -fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
  78.120 -
  78.121 -
  78.122 -(* naming *)
  78.123 -
  78.124 -fun name_multi name [x] = [(name, x)]
  78.125 -  | name_multi "" xs = map (pair "") xs
  78.126 -  | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
  78.127 -
  78.128 -fun name_thm pre official name thm = thm
  78.129 -  |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name
  78.130 -  |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
  78.131 -
  78.132 -fun name_thms pre official name xs =
  78.133 -  map (uncurry (name_thm pre official)) (name_multi name xs);
  78.134 -
  78.135 -fun name_thmss official name fact =
  78.136 -  burrow_fact (name_thms true official name) fact;
  78.137 -
  78.138 -
  78.139 -(* enter_thms *)
  78.140 -
  78.141 -fun enter_thms pre_name post_name app_att (b, thms) thy =
  78.142 -  if Binding.is_empty b
  78.143 -  then swap (register_proofs (app_att (thy, thms)))
  78.144 -  else
  78.145 -    let
  78.146 -      val naming = Sign.naming_of thy;
  78.147 -      val name = Name_Space.full_name naming b;
  78.148 -      val (thy', thms') =
  78.149 -        register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
  78.150 -      val thms'' = map (Thm.transfer thy') thms';
  78.151 -      val thy'' = thy' |> (Global_Facts.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
  78.152 -    in (thms'', thy'') end;
  78.153 -
  78.154 -
  78.155 -(* store_thm(s) *)
  78.156 -
  78.157 -fun store_thms (b, thms) =
  78.158 -  enter_thms (name_thms true true) (name_thms false true) I (b, thms);
  78.159 -
  78.160 -fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
  78.161 -
  78.162 -fun store_thm_open (b, th) =
  78.163 -  enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single;
  78.164 -
  78.165 -
  78.166 -(* add_thms(s) *)
  78.167 -
  78.168 -fun add_thms_atts pre_name ((b, thms), atts) =
  78.169 -  enter_thms pre_name (name_thms false true)
  78.170 -    (Library.foldl_map (Thm.theory_attributes atts)) (b, thms);
  78.171 -
  78.172 -fun gen_add_thmss pre_name =
  78.173 -  fold_map (add_thms_atts pre_name);
  78.174 -
  78.175 -fun gen_add_thms pre_name args =
  78.176 -  apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
  78.177 -
  78.178 -val add_thmss = gen_add_thmss (name_thms true true);
  78.179 -val add_thms = gen_add_thms (name_thms true true);
  78.180 -val add_thm = yield_singleton add_thms;
  78.181 -
  78.182 -
  78.183 -(* add_thms_dynamic *)
  78.184 -
  78.185 -fun add_thms_dynamic (b, f) thy = thy
  78.186 -  |> (Global_Facts.map o apfst)
  78.187 -      (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
  78.188 -
  78.189 -
  78.190 -(* note_thmss *)
  78.191 -
  78.192 -fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
  78.193 -  let
  78.194 -    val pos = Binding.pos_of b;
  78.195 -    val name = Sign.full_name thy b;
  78.196 -    val _ = Position.report pos (Markup.fact_decl name);
  78.197 -
  78.198 -    fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
  78.199 -    val (thms, thy') = thy |> enter_thms
  78.200 -      (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app)
  78.201 -      (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
  78.202 -  in ((name, thms), thy') end);
  78.203 -
  78.204 -
  78.205 -(* store axioms as theorems *)
  78.206 -
  78.207 -local
  78.208 -
  78.209 -fun no_read _ (_, t) = t;
  78.210 -
  78.211 -fun read thy (b, str) =
  78.212 -  Syntax.read_prop_global thy str handle ERROR msg =>
  78.213 -    cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
  78.214 -
  78.215 -fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
  78.216 -  let
  78.217 -    val prop = prep thy (b, raw_prop);
  78.218 -    val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
  78.219 -    val thm = def
  78.220 -      |> Thm.forall_intr_frees
  78.221 -      |> Thm.forall_elim_vars 0
  78.222 -      |> Thm.varifyT_global;
  78.223 -  in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end);
  78.224 -
  78.225 -in
  78.226 -
  78.227 -val add_defs = add no_read false;
  78.228 -val add_defs_unchecked = add no_read true;
  78.229 -val add_defs_cmd = add read false;
  78.230 -val add_defs_unchecked_cmd = add read true;
  78.231 -
  78.232 -end;
  78.233 -
  78.234 -
  78.235 -
  78.236 -(*** Pure theory syntax and logical content ***)
  78.237 -
  78.238  val typ = Simple_Syntax.read_typ;
  78.239  val prop = Simple_Syntax.read_prop;
  78.240  
  78.241 @@ -366,7 +149,7 @@
  78.242     [(Binding.name "term", typ "'a => prop", NoSyn),
  78.243      (Binding.name "sort_constraint", typ "'a itself => prop", NoSyn),
  78.244      (Binding.name "conjunction", typ "prop => prop => prop", NoSyn)]
  78.245 -  #> (add_defs false o map Thm.no_attributes)
  78.246 +  #> (Global_Theory.add_defs false o map Thm.no_attributes)
  78.247     [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
  78.248      (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
  78.249      (Binding.name "sort_constraint_def",
  78.250 @@ -376,7 +159,7 @@
  78.251    #> Sign.hide_const false "Pure.term"
  78.252    #> Sign.hide_const false "Pure.sort_constraint"
  78.253    #> Sign.hide_const false "Pure.conjunction"
  78.254 -  #> add_thmss [((Binding.name "nothing", []), [])] #> snd
  78.255 +  #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
  78.256    #> fold (fn (a, prop) => snd o Thm.add_axiom (Binding.name a, prop)) Proofterm.equality_axms));
  78.257  
  78.258  end;
    79.1 --- a/src/Sequents/Sequents.thy	Mon Sep 20 15:29:53 2010 +0200
    79.2 +++ b/src/Sequents/Sequents.thy	Mon Sep 20 16:05:25 2010 +0200
    79.3 @@ -10,7 +10,7 @@
    79.4  uses ("prover.ML")
    79.5  begin
    79.6  
    79.7 -setup PureThy.old_appl_syntax_setup
    79.8 +setup Pure_Thy.old_appl_syntax_setup
    79.9  
   79.10  declare [[unify_trace_bound = 20, unify_search_bound = 40]]
   79.11  
    80.1 --- a/src/ZF/Tools/datatype_package.ML	Mon Sep 20 15:29:53 2010 +0200
    80.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon Sep 20 16:05:25 2010 +0200
    80.3 @@ -242,17 +242,18 @@
    80.4    val need_recursor = (not coind andalso recursor_typ <> case_typ);
    80.5  
    80.6    fun add_recursor thy =
    80.7 -      if need_recursor then
    80.8 -           thy |> Sign.add_consts_i
    80.9 -                    [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
   80.10 -               |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
   80.11 -      else thy;
   80.12 +    if need_recursor then
   80.13 +      thy
   80.14 +      |> Sign.add_consts_i
   80.15 +        [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
   80.16 +      |> (snd o Global_Theory.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
   80.17 +    else thy;
   80.18  
   80.19    val (con_defs, thy0) = thy_path
   80.20               |> Sign.add_consts_i
   80.21                   (map (fn (c, T, mx) => (Binding.name c, T, mx))
   80.22                    ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
   80.23 -             |> PureThy.add_defs false
   80.24 +             |> Global_Theory.add_defs false
   80.25                   (map (Thm.no_attributes o apfst Binding.name)
   80.26                    (case_def ::
   80.27                     flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
   80.28 @@ -379,7 +380,7 @@
   80.29   in
   80.30    (*Updating theory components: simprules and datatype info*)
   80.31    (thy1 |> Sign.add_path big_rec_base_name
   80.32 -        |> PureThy.add_thmss
   80.33 +        |> Global_Theory.add_thmss
   80.34           [((Binding.name "simps", simps), [Simplifier.simp_add]),
   80.35            ((Binding.empty , intrs), [Classical.safe_intro NONE]),
   80.36            ((Binding.name "con_defs", con_defs), []),
    81.1 --- a/src/ZF/Tools/ind_cases.ML	Mon Sep 20 15:29:53 2010 +0200
    81.2 +++ b/src/ZF/Tools/ind_cases.ML	Mon Sep 20 16:05:25 2010 +0200
    81.3 @@ -50,7 +50,7 @@
    81.4      val facts = args |> map (fn ((name, srcs), props) =>
    81.5        ((name, map (Attrib.attribute thy) srcs),
    81.6          map (Thm.no_attributes o single o smart_cases ctxt) props));
    81.7 -  in thy |> PureThy.note_thmss "" facts |> snd end;
    81.8 +  in thy |> Global_Theory.note_thmss "" facts |> snd end;
    81.9  
   81.10  
   81.11  (* ind_cases method *)
    82.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Sep 20 15:29:53 2010 +0200
    82.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Sep 20 16:05:25 2010 +0200
    82.3 @@ -158,7 +158,7 @@
    82.4    in
    82.5      thy
    82.6      |> Sign.add_path (Long_Name.base_name big_rec_name)
    82.7 -    |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
    82.8 +    |> Global_Theory.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
    82.9      |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   82.10      |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
   82.11      |> Sign.parent_path
    83.1 --- a/src/ZF/Tools/inductive_package.ML	Mon Sep 20 15:29:53 2010 +0200
    83.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon Sep 20 16:05:25 2010 +0200
    83.3 @@ -172,7 +172,7 @@
    83.4    val (_, thy1) =
    83.5      thy
    83.6      |> Sign.add_path big_rec_base_name
    83.7 -    |> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
    83.8 +    |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
    83.9  
   83.10    val ctxt1 = ProofContext.init_global thy1;
   83.11  
   83.12 @@ -508,7 +508,7 @@
   83.13  
   83.14       val ([induct', mutual_induct'], thy') =
   83.15         thy
   83.16 -       |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), induct),
   83.17 +       |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), induct),
   83.18               [case_names, Induct.induct_pred big_rec_name]),
   83.19             ((Binding.name "mutual_induct", mutual_induct), [case_names])];
   83.20      in ((thy', induct'), mutual_induct')
   83.21 @@ -520,7 +520,7 @@
   83.22      if not coind then induction_rules raw_induct thy1
   83.23      else
   83.24        (thy1
   83.25 -      |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
   83.26 +      |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
   83.27        |> apfst hd |> Library.swap, @{thm TrueI})
   83.28    and defs = big_rec_def :: part_rec_defs
   83.29  
   83.30 @@ -528,16 +528,16 @@
   83.31    val (([bnd_mono', dom_subset', elim'], [defs', intrs']), thy3) =
   83.32      thy2
   83.33      |> IndCases.declare big_rec_name make_cases
   83.34 -    |> PureThy.add_thms
   83.35 +    |> Global_Theory.add_thms
   83.36        [((Binding.name "bnd_mono", bnd_mono), []),
   83.37         ((Binding.name "dom_subset", dom_subset), []),
   83.38         ((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])]
   83.39 -    ||>> (PureThy.add_thmss o map Thm.no_attributes)
   83.40 +    ||>> (Global_Theory.add_thmss o map Thm.no_attributes)
   83.41          [(Binding.name "defs", defs),
   83.42           (Binding.name "intros", intrs)];
   83.43    val (intrs'', thy4) =
   83.44      thy3
   83.45 -    |> PureThy.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs)
   83.46 +    |> Global_Theory.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs)
   83.47      ||> Sign.parent_path;
   83.48    in
   83.49      (thy4,
    84.1 --- a/src/ZF/Tools/primrec_package.ML	Mon Sep 20 15:29:53 2010 +0200
    84.2 +++ b/src/ZF/Tools/primrec_package.ML	Mon Sep 20 16:05:25 2010 +0200
    84.3 @@ -169,7 +169,7 @@
    84.4  
    84.5      val ([def_thm], thy1) = thy
    84.6        |> Sign.add_path (Long_Name.base_name fname)
    84.7 -      |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
    84.8 +      |> Global_Theory.add_defs false [Thm.no_attributes (apfst Binding.name def)];
    84.9  
   84.10      val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
   84.11      val eqn_thms =
   84.12 @@ -179,10 +179,10 @@
   84.13  
   84.14      val (eqn_thms', thy2) =
   84.15        thy1
   84.16 -      |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
   84.17 +      |> Global_Theory.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
   84.18      val (_, thy3) =
   84.19        thy2
   84.20 -      |> PureThy.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])]
   84.21 +      |> Global_Theory.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])]
   84.22        ||> Sign.parent_path;
   84.23    in (thy3, eqn_thms') end;
   84.24