# HG changeset patch # User wenzelm # Date 1284991525 -7200 # Node ID fe5722fce758ef2b2a8cd2fcb4f40bd982d6c712 # Parent 32a00ff29d1a0a5833784abdceb868e62adaae8c renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only; diff -r 32a00ff29d1a -r fe5722fce758 NEWS --- a/NEWS Mon Sep 20 15:29:53 2010 +0200 +++ b/NEWS Mon Sep 20 16:05:25 2010 +0200 @@ -244,6 +244,10 @@ *** ML *** +* Renamed structure PureThy to Pure_Thy and moved most of its +operations to structure Global_Theory, to emphasize that this is +rarely-used global-only stuff. + * Discontinued Output.debug. Minor INCOMPATIBILITY, use plain writeln instead (or tracing for high-volume output). diff -r 32a00ff29d1a -r fe5722fce758 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Mon Sep 20 15:29:53 2010 +0200 +++ b/src/CTT/CTT.thy Mon Sep 20 16:05:25 2010 +0200 @@ -10,7 +10,7 @@ uses "~~/src/Provers/typedsimp.ML" ("rew.ML") begin -setup PureThy.old_appl_syntax_setup +setup Pure_Thy.old_appl_syntax_setup typedecl i typedecl t diff -r 32a00ff29d1a -r fe5722fce758 src/Cube/Cube.thy --- a/src/Cube/Cube.thy Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Cube/Cube.thy Mon Sep 20 16:05:25 2010 +0200 @@ -8,7 +8,7 @@ imports Pure begin -setup PureThy.old_appl_syntax_setup +setup Pure_Thy.old_appl_syntax_setup typedecl "term" typedecl "context" diff -r 32a00ff29d1a -r fe5722fce758 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Mon Sep 20 15:29:53 2010 +0200 +++ b/src/FOL/IFOL.thy Mon Sep 20 16:05:25 2010 +0200 @@ -26,7 +26,7 @@ subsection {* Syntax and axiomatic basis *} -setup PureThy.old_appl_syntax_setup +setup Pure_Thy.old_appl_syntax_setup classes "term" default_sort "term" diff -r 32a00ff29d1a -r fe5722fce758 src/FOL/ex/Locale_Test/Locale_Test1.thy --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Sep 20 15:29:53 2010 +0200 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Sep 20 16:05:25 2010 +0200 @@ -442,7 +442,7 @@ interpretation int2?: semi "op +" by unfold_locales (* subsumed, thm int2.assoc not generated *) -ML {* (PureThy.get_thms @{theory} "int2.assoc"; +ML {* (Global_Theory.get_thms @{theory} "int2.assoc"; error "thm int2.assoc was generated") handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *} diff -r 32a00ff29d1a -r fe5722fce758 src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Mon Sep 20 15:29:53 2010 +0200 +++ b/src/FOLP/IFOLP.thy Mon Sep 20 16:05:25 2010 +0200 @@ -10,7 +10,7 @@ uses ("hypsubst.ML") ("intprover.ML") begin -setup PureThy.old_appl_syntax_setup +setup Pure_Thy.old_appl_syntax_setup classes "term" default_sort "term" diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Import/hol4rews.ML Mon Sep 20 16:05:25 2010 +0200 @@ -370,7 +370,7 @@ val thm2 = Drule.export_without_context thm1; in thy - |> PureThy.store_thm (Binding.name bthm, thm2) + |> Global_Theory.store_thm (Binding.name bthm, thm2) |> snd |> add_hol4_theorem bthy bthm hth end; diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Import/proof_kernel.ML Mon Sep 20 16:05:25 2010 +0200 @@ -1261,10 +1261,10 @@ case get_hol4_mapping thyname thmname thy of SOME (SOME thmname) => let - val th1 = (SOME (PureThy.get_thm thy thmname) + val th1 = (SOME (Global_Theory.get_thm thy thmname) handle ERROR _ => (case split_name thmname of - SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1)) + SOME (listname,idx) => (SOME (List.nth(Global_Theory.get_thms thy listname,idx-1)) handle _ => NONE) (* FIXME avoid handle _ *) | NONE => NONE)) in @@ -1922,7 +1922,7 @@ | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy) val eq = mk_defeq constname rhs' thy1 - val (thms, thy2) = PureThy.add_defs false [((Binding.name thmname,eq),[])] thy1 + val (thms, thy2) = Global_Theory.add_defs false [((Binding.name thmname,eq),[])] thy1 val _ = ImportRecorder.add_defs thmname eq val def_thm = hd thms val thm' = def_thm RS meta_eq_to_obj_eq_thm @@ -2144,7 +2144,7 @@ fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy = case HOL4DefThy.get thy of Replaying _ => (thy, - HOLThm([], PureThy.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth) + HOLThm([], Global_Theory.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth) | _ => let val _ = message "TYPE_INTRO:" diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Import/replay.ML --- a/src/HOL/Import/replay.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Import/replay.ML Mon Sep 20 16:05:25 2010 +0200 @@ -339,7 +339,7 @@ | delta (Hol_move (fullname, moved_thmname)) thy = add_hol4_move fullname moved_thmname thy | delta (Defs (thmname, eq)) thy = - snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy) + snd (Global_Theory.add_defs false [((Binding.name thmname, eq), [])] thy) | delta (Hol_theorem (thyname, thmname, th)) thy = add_hol4_theorem thyname thmname ([], th_of thy th) thy | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Import/shuffler.ML Mon Sep 20 16:05:25 2010 +0200 @@ -623,7 +623,7 @@ val shuffles = ShuffleData.get thy val ignored = collect_ignored shuffles [] val all_thms = - map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy))) + map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (Global_Theory.facts_of thy))) in filter (match_consts ignored t) all_thms end diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Mon Sep 20 16:05:25 2010 +0200 @@ -183,7 +183,7 @@ fun theorems_in_proof_term thm = let - val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm) + val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm) fun collect (s, _, _) = if s <> "" then insert (op =) s else I fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE fun resolve_thms names = map_filter (member_of names) all_thms diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Mutabelle/Mutabelle.thy --- a/src/HOL/Mutabelle/Mutabelle.thy Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Mutabelle/Mutabelle.thy Mon Sep 20 16:05:25 2010 +0200 @@ -75,12 +75,12 @@ fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso is_executable thy th) - (PureThy.all_thms_of thy); + (Global_Theory.all_thms_of thy); fun find_thm thy = find_first (fn (_, th) => not (Thm.is_internal th) andalso Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso is_executable thy th) - (PureThy.all_thms_of thy); + (Global_Theory.all_thms_of thy); *} ML {* diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Mutabelle/mutabelle.ML Mon Sep 20 16:05:25 2010 +0200 @@ -59,7 +59,7 @@ fun all_unconcealed_thms_of thy = let - val facts = PureThy.facts_of thy + val facts = Global_Theory.facts_of thy in Facts.fold_static (fn (s, ths) => diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Mon Sep 20 16:05:25 2010 +0200 @@ -88,8 +88,8 @@ let val T = fastype_of x in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end; -fun add_thms_string args = PureThy.add_thms ((map o apfst o apfst) Binding.name args); -fun add_thmss_string args = PureThy.add_thmss ((map o apfst o apfst) Binding.name args); +fun add_thms_string args = Global_Theory.add_thms ((map o apfst o apfst) Binding.name args); +fun add_thmss_string args = Global_Theory.add_thmss ((map o apfst o apfst) Binding.name args); (* this function sets up all matters related to atom- *) (* kinds; the user specifies a list of atom-kind names *) @@ -189,7 +189,7 @@ val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c) in thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)] - |> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])] + |> Global_Theory.add_defs_unchecked true [((Binding.name name, def2),[])] |> snd |> OldPrimrec.add_primrec_unchecked_i "" [(("", def1),[])] end) ak_names_types thy1; @@ -244,7 +244,7 @@ val def = Logic.mk_equals (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a) in - PureThy.add_defs_unchecked true [((Binding.name name, def),[])] thy' + Global_Theory.add_defs_unchecked true [((Binding.name name, def),[])] thy' end) ak_names_types thy) ak_names_types thy4; (* proves that every atom-kind is an instance of at *) @@ -257,7 +257,7 @@ val i_type = Type(ak_name_qu,[]); val cat = Const ("Nominal.at",(Term.itselfT i_type) --> HOLogic.boolT); val at_type = Logic.mk_type i_type; - val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy5) + val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy5) ["at_def", ak_name ^ "_prm_" ^ ak_name ^ "_def", ak_name ^ "_prm_" ^ ak_name ^ ".simps", @@ -321,7 +321,7 @@ val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); val pt_type = Logic.mk_type i_type1; val at_type = Logic.mk_type i_type2; - val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy7) + val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy7) ["pt_def", "pt_" ^ ak_name ^ "1", "pt_" ^ ak_name ^ "2", @@ -369,7 +369,7 @@ (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); val fs_type = Logic.mk_type i_type1; val at_type = Logic.mk_type i_type2; - val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy11) + val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy11) ["fs_def", "fs_" ^ ak_name ^ "1"]; @@ -422,8 +422,8 @@ val at_type = Logic.mk_type i_type1; val at_type' = Logic.mk_type i_type2; val cp_type = Logic.mk_type i_type0; - val simp_s = HOL_basic_ss addsimps maps (PureThy.get_thms thy') ["cp_def"]; - val cp1 = PureThy.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1"); + val simp_s = HOL_basic_ss addsimps maps (Global_Theory.get_thms thy') ["cp_def"]; + val cp1 = Global_Theory.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1"); val name = "cp_"^ak_name^ "_"^ak_name'^"_inst"; val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type'); @@ -454,7 +454,7 @@ (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); val at_type = Logic.mk_type i_type1; val at_type' = Logic.mk_type i_type2; - val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy') + val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy') ["disjoint_def", ak_name ^ "_prm_" ^ ak_name' ^ "_def", ak_name' ^ "_prm_" ^ ak_name ^ "_def"]; @@ -493,7 +493,7 @@ let val qu_name = Sign.full_bname thy' ak_name'; val cls_name = Sign.full_bname thy' ("pt_"^ak_name); - val at_inst = PureThy.get_thm thy' ("at_" ^ ak_name' ^ "_inst"); + val at_inst = Global_Theory.get_thm thy' ("at_" ^ ak_name' ^ "_inst"); val proof1 = EVERY [Class.intro_classes_tac [], rtac ((at_inst RS at_pt_inst) RS pt1) 1, @@ -501,7 +501,7 @@ rtac ((at_inst RS at_pt_inst) RS pt3) 1, atac 1]; val simp_s = HOL_basic_ss addsimps - maps (PureThy.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"]; + maps (Global_Theory.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"]; val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; in @@ -523,8 +523,8 @@ val thy18 = fold (fn ak_name => fn thy => let val cls_name = Sign.full_bname thy ("pt_"^ak_name); - val at_thm = PureThy.get_thm thy ("at_"^ak_name^"_inst"); - val pt_inst = PureThy.get_thm thy ("pt_"^ak_name^"_inst"); + val at_thm = Global_Theory.get_thm thy ("at_"^ak_name^"_inst"); + val pt_inst = Global_Theory.get_thm thy ("pt_"^ak_name^"_inst"); fun pt_proof thm = EVERY [Class.intro_classes_tac [], @@ -571,11 +571,11 @@ val proof = (if ak_name = ak_name' then - let val at_thm = PureThy.get_thm thy' ("at_"^ak_name^"_inst"); + let val at_thm = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); in EVERY [Class.intro_classes_tac [], rtac ((at_thm RS fs_at_inst) RS fs1) 1] end else - let val dj_inst = PureThy.get_thm thy' ("dj_"^ak_name'^"_"^ak_name); + let val dj_inst = Global_Theory.get_thm thy' ("dj_"^ak_name'^"_"^ak_name); val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI]; in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end) in @@ -593,7 +593,7 @@ val thy24 = fold (fn ak_name => fn thy => let val cls_name = Sign.full_bname thy ("fs_"^ak_name); - val fs_inst = PureThy.get_thm thy ("fs_"^ak_name^"_inst"); + val fs_inst = Global_Theory.get_thm thy ("fs_"^ak_name^"_inst"); fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1]; val fs_thm_unit = fs_unit_inst; @@ -637,18 +637,18 @@ val proof = (if (ak_name'=ak_name'') then (let - val pt_inst = PureThy.get_thm thy'' ("pt_"^ak_name''^"_inst"); - val at_inst = PureThy.get_thm thy'' ("at_"^ak_name''^"_inst"); + val pt_inst = Global_Theory.get_thm thy'' ("pt_"^ak_name''^"_inst"); + val at_inst = Global_Theory.get_thm thy'' ("at_"^ak_name''^"_inst"); in EVERY [Class.intro_classes_tac [], rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1] end) else (let - val dj_inst = PureThy.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name'); + val dj_inst = Global_Theory.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name'); val simp_s = HOL_basic_ss addsimps ((dj_inst RS dj_pp_forget):: - (maps (PureThy.get_thms thy'') + (maps (Global_Theory.get_thms thy'') [ak_name' ^"_prm_"^ak_name^"_def", ak_name''^"_prm_"^ak_name^"_def"])); in @@ -671,9 +671,9 @@ fold (fn ak_name' => fn thy' => let val cls_name = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name'); - val cp_inst = PureThy.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst"); - val pt_inst = PureThy.get_thm thy' ("pt_"^ak_name^"_inst"); - val at_inst = PureThy.get_thm thy' ("at_"^ak_name^"_inst"); + val cp_inst = Global_Theory.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst"); + val pt_inst = Global_Theory.get_thm thy' ("pt_"^ak_name^"_inst"); + val at_inst = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); fun cp_proof thm = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1]; @@ -839,27 +839,27 @@ (* list of all at_inst-theorems *) - val ats = map (fn ak => PureThy.get_thm thy32 ("at_"^ak^"_inst")) ak_names + val ats = map (fn ak => Global_Theory.get_thm thy32 ("at_"^ak^"_inst")) ak_names (* list of all pt_inst-theorems *) - val pts = map (fn ak => PureThy.get_thm thy32 ("pt_"^ak^"_inst")) ak_names + val pts = map (fn ak => Global_Theory.get_thm thy32 ("pt_"^ak^"_inst")) ak_names (* list of all cp_inst-theorems as a collection of lists*) val cps = - let fun cps_fun ak1 ak2 = PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst") + let fun cps_fun ak1 ak2 = Global_Theory.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst") in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; (* list of all cp_inst-theorems that have different atom types *) val cps' = let fun cps'_fun ak1 ak2 = - if ak1=ak2 then NONE else SOME (PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")) + if ak1=ak2 then NONE else SOME (Global_Theory.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")) in map (fn aki => (map_filter I (map (cps'_fun aki) ak_names))) ak_names end; (* list of all dj_inst-theorems *) val djs = let fun djs_fun ak1 ak2 = - if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 ("dj_"^ak2^"_"^ak1)) + if ak1=ak2 then NONE else SOME(Global_Theory.get_thm thy32 ("dj_"^ak2^"_"^ak1)) in map_filter I (map_product djs_fun ak_names ak_names) end; (* list of all fs_inst-theorems *) - val fss = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"_inst")) ak_names + val fss = map (fn ak => Global_Theory.get_thm thy32 ("fs_"^ak^"_inst")) ak_names (* list of all at_inst-theorems *) - val fs_axs = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"1")) ak_names + val fs_axs = map (fn ak => Global_Theory.get_thm thy32 ("fs_"^ak^"1")) ak_names fun inst_pt thms = maps (fn ti => instR ti pts) thms; fun inst_at thms = maps (fn ti => instR ti ats) thms; diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Mon Sep 20 16:05:25 2010 +0200 @@ -306,7 +306,7 @@ val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names)); val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); - val perm_fun_def = PureThy.get_thm thy2 "perm_fun_def"; + val perm_fun_def = Global_Theory.get_thm thy2 "perm_fun_def"; val unfolded_perm_eq_thms = if length descr = length new_type_names then [] @@ -351,8 +351,8 @@ val _ = warning "perm_append_thms"; (*FIXME: these should be looked up statically*) - val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst"; - val pt2 = PureThy.get_thm thy2 "pt2"; + val at_pt_inst = Global_Theory.get_thm thy2 "at_pt_inst"; + val pt2 = Global_Theory.get_thm thy2 "pt2"; val perm_append_thms = maps (fn a => let @@ -361,7 +361,7 @@ val pi2 = Free ("pi2", permT); val pt_inst = pt_inst_of thy2 a; val pt2' = pt_inst RS pt2; - val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a); + val pt2_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a); in List.take (map Drule.export_without_context (split_conj_thm (Goal.prove_global thy2 [] [] (augment_sort thy2 [pt_class_of thy2 a] @@ -384,8 +384,8 @@ val _ = warning "perm_eq_thms"; - val pt3 = PureThy.get_thm thy2 "pt3"; - val pt3_rev = PureThy.get_thm thy2 "pt3_rev"; + val pt3 = Global_Theory.get_thm thy2 "pt3"; + val pt3_rev = Global_Theory.get_thm thy2 "pt3_rev"; val perm_eq_thms = maps (fn a => let @@ -396,7 +396,7 @@ val pt_inst = pt_inst_of thy2 a; val pt3' = pt_inst RS pt3; val pt3_rev' = at_inst RS (pt_inst RS pt3_rev); - val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a); + val pt3_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a); in List.take (map Drule.export_without_context (split_conj_thm (Goal.prove_global thy2 [] [] (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies @@ -418,11 +418,11 @@ (**** prove pi1 \ (pi2 \ t) = (pi1 \ pi2) \ (pi1 \ t) ****) - val cp1 = PureThy.get_thm thy2 "cp1"; - val dj_cp = PureThy.get_thm thy2 "dj_cp"; - val pt_perm_compose = PureThy.get_thm thy2 "pt_perm_compose"; - val pt_perm_compose_rev = PureThy.get_thm thy2 "pt_perm_compose_rev"; - val dj_perm_perm_forget = PureThy.get_thm thy2 "dj_perm_perm_forget"; + val cp1 = Global_Theory.get_thm thy2 "cp1"; + val dj_cp = Global_Theory.get_thm thy2 "dj_cp"; + val pt_perm_compose = Global_Theory.get_thm thy2 "pt_perm_compose"; + val pt_perm_compose_rev = Global_Theory.get_thm thy2 "pt_perm_compose_rev"; + val dj_perm_perm_forget = Global_Theory.get_thm thy2 "dj_perm_perm_forget"; fun composition_instance name1 name2 thy = let @@ -486,7 +486,7 @@ resolve_tac perm_eq_thms 1, assume_tac 1]) thy) (full_new_type_names' ~~ tyvars) thy end) atoms |> - PureThy.add_thmss + Global_Theory.add_thmss [((Binding.name (space_implode "_" new_type_names ^ "_unfolded_perm_eq"), unfolded_perm_eq_thms), [Simplifier.simp_add]), ((Binding.name (space_implode "_" new_type_names ^ "_perm_empty"), @@ -578,7 +578,7 @@ val _ = warning "proving closure under permutation..."; - val abs_perm = PureThy.get_thms thy4 "abs_perm"; + val abs_perm = Global_Theory.get_thms thy4 "abs_perm"; val perm_indnames' = map_filter (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x) @@ -626,7 +626,7 @@ val pi = Free ("pi", permT); val T = Type (Sign.intern_type thy name, map TFree tvs); in apfst (pair r o hd) - (PureThy.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals + (Global_Theory.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T), Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $ (Const ("Nominal.perm", permT --> U --> U) $ pi $ @@ -662,7 +662,7 @@ asm_full_simp_tac (global_simpset_of thy addsimps [Rep_inverse]) 1, asm_full_simp_tac (global_simpset_of thy addsimps [Rep RS perm_closed RS Abs_inverse]) 1, - asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy + asm_full_simp_tac (HOL_basic_ss addsimps [Global_Theory.get_thm thy ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy end) (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ @@ -801,7 +801,7 @@ val def_name = (Long_Name.base_name cname) ^ "_def"; val ([def_thm], thy') = thy |> Sign.add_consts_i [(Binding.name cname', constrT, mx)] |> - (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)] + (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)] in (thy', defs @ [def_thm], eqns @ [eqn]) end; fun dt_constr_defs ((((((_, (_, _, constrs)), @@ -935,8 +935,8 @@ (** prove injectivity of constructors **) val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms; - val alpha = PureThy.get_thms thy8 "alpha"; - val abs_fresh = PureThy.get_thms thy8 "abs_fresh"; + val alpha = Global_Theory.get_thms thy8 "alpha"; + val abs_fresh = Global_Theory.get_thms thy8 "abs_fresh"; val pt_cp_sort = map (pt_class_of thy8) dt_atoms @ @@ -1087,8 +1087,8 @@ val indnames = Datatype_Prop.make_tnames recTs; - val abs_supp = PureThy.get_thms thy8 "abs_supp"; - val supp_atm = PureThy.get_thms thy8 "supp_atm"; + val abs_supp = Global_Theory.get_thms thy8 "abs_supp"; + val supp_atm = Global_Theory.get_thms thy8 "supp_atm"; val finite_supp_thms = map (fn atom => let val atomT = Type (atom, []) @@ -1103,7 +1103,7 @@ (fn _ => indtac dt_induct indnames 1 THEN ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps (abs_supp @ supp_atm @ - PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @ + Global_Theory.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @ flat supp_thms))))), length new_type_names)) end) atoms; @@ -1117,8 +1117,8 @@ val (_, thy9) = thy8 |> Sign.add_path big_name |> - PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>> - PureThy.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||> + Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>> + Global_Theory.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||> Sign.parent_path ||>> Datatype_Aux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>> Datatype_Aux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>> @@ -1235,17 +1235,17 @@ val fin_set_fresh = map (fn s => at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms; val pt1_atoms = map (fn Type (s, _) => - PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs; + Global_Theory.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs; val pt2_atoms = map (fn Type (s, _) => - PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs; - val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'"; - val fs_atoms = PureThy.get_thms thy9 "fin_supp"; - val abs_supp = PureThy.get_thms thy9 "abs_supp"; - val perm_fresh_fresh = PureThy.get_thms thy9 "perm_fresh_fresh"; - val calc_atm = PureThy.get_thms thy9 "calc_atm"; - val fresh_atm = PureThy.get_thms thy9 "fresh_atm"; - val fresh_left = PureThy.get_thms thy9 "fresh_left"; - val perm_swap = PureThy.get_thms thy9 "perm_swap"; + Global_Theory.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs; + val exists_fresh' = Global_Theory.get_thms thy9 "exists_fresh'"; + val fs_atoms = Global_Theory.get_thms thy9 "fin_supp"; + val abs_supp = Global_Theory.get_thms thy9 "abs_supp"; + val perm_fresh_fresh = Global_Theory.get_thms thy9 "perm_fresh_fresh"; + val calc_atm = Global_Theory.get_thms thy9 "calc_atm"; + val fresh_atm = Global_Theory.get_thms thy9 "fresh_atm"; + val fresh_left = Global_Theory.get_thms thy9 "fresh_left"; + val perm_swap = Global_Theory.get_thms thy9 "perm_swap"; fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) = let @@ -1408,9 +1408,9 @@ val (_, thy10) = thy9 |> Sign.add_path big_name |> - PureThy.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>> - PureThy.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>> - PureThy.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])]; + Global_Theory.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>> + Global_Theory.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>> + Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])]; (**** recursion combinator ****) @@ -1517,13 +1517,13 @@ (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] - ||> PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct") + ||> Global_Theory.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct") ||> Sign.restore_naming thy10; (** equivariance **) - val fresh_bij = PureThy.get_thms thy11 "fresh_bij"; - val perm_bij = PureThy.get_thms thy11 "perm_bij"; + val fresh_bij = Global_Theory.get_thms thy11 "fresh_bij"; + val perm_bij = Global_Theory.get_thms thy11 "perm_bij"; val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT => let @@ -1565,7 +1565,7 @@ val rec_fin_supp_thms = map (fn aT => let val name = Long_Name.base_name (fst (dest_Type aT)); - val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1"); + val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1"); val aset = HOLogic.mk_setT aT; val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT); val fins = map (fn (f, T) => HOLogic.mk_Trueprop @@ -1604,7 +1604,7 @@ val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) => let val name = Long_Name.base_name (fst (dest_Type aT)); - val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1"); + val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1"); val a = Free ("a", aT); val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop (fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts) @@ -2018,7 +2018,7 @@ |> Sign.add_consts_i (map (fn ((name, T), T') => (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) - |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => + |> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', set $ Free ("x", T) $ Free ("y", T')))))) @@ -2055,7 +2055,7 @@ (* FIXME: theorems are stored in database for testing only *) val (_, thy13) = thy12 |> - PureThy.add_thmss + Global_Theory.add_thmss [((Binding.name "rec_equiv", flat rec_equiv_thms), []), ((Binding.name "rec_equiv'", flat rec_equiv_thms'), []), ((Binding.name "rec_fin_supp", flat rec_fin_supp_thms), []), diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Mon Sep 20 16:05:25 2010 +0200 @@ -37,7 +37,7 @@ res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th); fun get_dyn_thm thy name atom_name = - PureThy.get_thm thy name handle ERROR _ => + Global_Theory.get_thm thy name handle ERROR _ => error ("The atom type "^atom_name^" is not defined."); (* End of function waiting to be in the library :o) *) @@ -126,8 +126,8 @@ val thy = theory_of_thm thm; val ctxt = ProofContext.init_global thy; val ss = global_simpset_of thy; - val abs_fresh = PureThy.get_thms thy "abs_fresh"; - val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app"; + val abs_fresh = Global_Theory.get_thms thy "abs_fresh"; + val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app"; val ss' = ss addsimps fresh_prod::abs_fresh; val ss'' = ss' addsimps fresh_perm_app; val x = hd (tl (OldTerm.term_vars (prop_of exI))); diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Mon Sep 20 16:05:25 2010 +0200 @@ -271,21 +271,21 @@ (NominalDatatype.fresh_const U T $ u $ t)) bvars) (ts ~~ binder_types (fastype_of p)))) prems; - val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; - val pt2_atoms = map (fn aT => PureThy.get_thm thy + val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; + val pt2_atoms = map (fn aT => Global_Theory.get_thm thy ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs; val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc ["Fun.id"], NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; - val fresh_bij = PureThy.get_thms thy "fresh_bij"; - val perm_bij = PureThy.get_thms thy "perm_bij"; - val fs_atoms = map (fn aT => PureThy.get_thm thy + val fresh_bij = Global_Theory.get_thms thy "fresh_bij"; + val perm_bij = Global_Theory.get_thms thy "perm_bij"; + val fs_atoms = map (fn aT => Global_Theory.get_thm thy ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs; - val exists_fresh' = PureThy.get_thms thy "exists_fresh'"; - val fresh_atm = PureThy.get_thms thy "fresh_atm"; - val swap_simps = PureThy.get_thms thy "swap_simps"; - val perm_fresh_fresh = PureThy.get_thms thy "perm_fresh_fresh"; + val exists_fresh' = Global_Theory.get_thms thy "exists_fresh'"; + val fresh_atm = Global_Theory.get_thms thy "fresh_atm"; + val swap_simps = Global_Theory.get_thms thy "swap_simps"; + val perm_fresh_fresh = Global_Theory.get_thms thy "perm_fresh_fresh"; fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) = let @@ -610,7 +610,7 @@ | xs => error ("No such atoms: " ^ commas xs); atoms) end; - val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; + val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs [mk_perm_bool_simproc names, diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Sep 20 16:05:25 2010 +0200 @@ -290,14 +290,14 @@ HOLogic.mk_setT U --> HOLogic.boolT) $ u)) sets) |> split_list) prems |> split_list; - val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; - val pt2_atoms = map (fn a => PureThy.get_thm thy + val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; + val pt2_atoms = map (fn a => Global_Theory.get_thm thy ("pt_" ^ Long_Name.base_name a ^ "2")) atoms; val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc ["Fun.id"], NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; - val fresh_star_bij = PureThy.get_thms thy "fresh_star_bij"; + val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij"; val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms; val at_insts = map (NominalAtoms.at_inst_of thy) atoms; val dj_thms = maps (fn a => @@ -319,7 +319,7 @@ val p = foldr1 HOLogic.mk_prod (map protect ts); val atom = fst (dest_Type T); val {at_inst, ...} = NominalAtoms.the_atom_info thy atom; - val fs_atom = PureThy.get_thm thy + val fs_atom = Global_Theory.get_thm thy ("fs_" ^ Long_Name.base_name atom ^ "1"); val avoid_th = Drule.instantiate' [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)] diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Mon Sep 20 16:05:25 2010 +0200 @@ -71,8 +71,8 @@ val supports_fresh_rule = @{thm "supports_fresh"}; (* pulls out dynamically a thm via the proof state *) -fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) name; -fun dynamic_thm st name = PureThy.get_thm (theory_of_thm st) name; +fun dynamic_thms st name = Global_Theory.get_thms (theory_of_thm st) name; +fun dynamic_thm st name = Global_Theory.get_thm (theory_of_thm st) name; (* needed in the process of fully simplifying permutations *) @@ -107,8 +107,8 @@ (if (applicable_app f) then let val name = Long_Name.base_name n - val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst") - val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst") + val at_inst = Global_Theory.get_thm sg ("at_" ^ name ^ "_inst") + val pt_inst = Global_Theory.get_thm sg ("pt_" ^ name ^ "_inst") in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end else NONE) | _ => NONE @@ -202,13 +202,13 @@ SOME (Drule.instantiate' [SOME (ctyp_of sg (fastype_of t))] [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)] - (mk_meta_eq ([PureThy.get_thm sg ("pt_"^tname'^"_inst"), - PureThy.get_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux))) + (mk_meta_eq ([Global_Theory.get_thm sg ("pt_"^tname'^"_inst"), + Global_Theory.get_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux))) else SOME (Drule.instantiate' [SOME (ctyp_of sg (fastype_of t))] [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)] - (mk_meta_eq (PureThy.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS + (mk_meta_eq (Global_Theory.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS cp1_aux))) else NONE end diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon Sep 20 16:05:25 2010 +0200 @@ -56,7 +56,7 @@ val mypi = Thm.cterm_of thy pi val T = fastype_of pi' val mypifree = Thm.cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi') - val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp" + val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp" in EVERY1 [tactic ctxt ("iffI applied", rtac @{thm iffI}), tactic ctxt ("remove pi with perm_boolE", dtac @{thm perm_boolE}), @@ -175,7 +175,7 @@ "equivariance theorem declaration" #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del) "equivariance theorem declaration (without checking the form of the lemma)" #> - PureThy.add_thms_dynamic (@{binding eqvts}, Data.get); + Global_Theory.add_thms_dynamic (@{binding eqvts}, Data.get); end; diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Statespace/DistinctTreeProver.thy --- a/src/HOL/Statespace/DistinctTreeProver.thy Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Mon Sep 20 16:05:25 2010 +0200 @@ -671,7 +671,7 @@ setup {* Theory.add_consts_i const_decls -#> (fn thy => let val ([thm],thy') = PureThy.add_axioms [(("dist_axiom",dist),[])] thy +#> (fn thy => let val ([thm],thy') = Global_Theory.add_axioms [(("dist_axiom",dist),[])] thy in (da := thm; thy') end) *} diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/String.thy --- a/src/HOL/String.thy Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/String.thy Mon Sep 20 16:05:25 2010 +0200 @@ -53,7 +53,8 @@ (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps}) nibbles nibbles; in - PureThy.note_thmss Thm.definitionK [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])] + Global_Theory.note_thmss Thm.definitionK + [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])] #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms) end *} diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Mon Sep 20 16:05:25 2010 +0200 @@ -241,7 +241,7 @@ val ([def_thm], thy') = thy |> Sign.add_consts_i [(cname', constrT, mx)] - |> (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]; + |> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]; in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end; @@ -352,7 +352,7 @@ Logic.mk_equals (Const (iso_name, T --> Univ_elT), list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos); val (def_thms, thy') = - apsnd Theory.checkpoint ((PureThy.add_defs false o map Thm.no_attributes) defs thy); + apsnd Theory.checkpoint ((Global_Theory.add_defs false o map Thm.no_attributes) defs thy); (* prove characteristic equations *) @@ -628,7 +628,7 @@ val ([dt_induct'], thy7) = thy6 |> Sign.add_path big_name - |> PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] + |> Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||> Sign.parent_path ||> Theory.checkpoint; diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Sep 20 16:05:25 2010 +0200 @@ -234,11 +234,13 @@ |> Sign.add_consts_i (map (fn ((name, T), T') => (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) - |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => - (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, - Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', - set $ Free ("x", T) $ Free ("y", T')))))) - (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) + |> (Global_Theory.add_defs false o map Thm.no_attributes) + (map (fn ((((name, comb), set), T), T') => + (Binding.name (Long_Name.base_name name ^ "_def"), + Logic.mk_equals (comb, absfree ("x", T, + Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', + set $ Free ("x", T) $ Free ("y", T')))))) + (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) ||> Sign.parent_path ||> Theory.checkpoint; @@ -259,7 +261,7 @@ in thy2 |> Sign.add_path (space_implode "_" new_type_names) - |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])] + |> Global_Theory.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])] ||> Sign.parent_path ||> Theory.checkpoint |-> (fn thms => pair (reccomb_names, flat thms)) @@ -319,7 +321,7 @@ val ([def_thm], thy') = thy |> Sign.declare_const decl |> snd - |> (PureThy.add_defs false o map Thm.no_attributes) [def]; + |> (Global_Theory.add_defs false o map Thm.no_attributes) [def]; in (defs @ [def_thm], thy') end) (hd descr ~~ newTs ~~ case_names ~~ diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Mon Sep 20 16:05:25 2010 +0200 @@ -99,7 +99,7 @@ fun store_thmss_atts label tnames attss thmss = fold_map (fn ((tname, atts), thms) => Sign.add_path tname - #> PureThy.add_thmss [((Binding.name label, thms), atts)] + #> Global_Theory.add_thmss [((Binding.name label, thms), atts)] #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss) ##> Theory.checkpoint; @@ -108,7 +108,7 @@ fun store_thms_atts label tnames attss thmss = fold_map (fn ((tname, atts), thms) => Sign.add_path tname - #> PureThy.add_thms [((Binding.name label, thms), atts)] + #> Global_Theory.add_thms [((Binding.name label, thms), atts)] #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss) ##> Theory.checkpoint; diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Sep 20 16:05:25 2010 +0200 @@ -109,7 +109,7 @@ fun add_eq_thms tyco = Theory.checkpoint #> `(fn thy => mk_eq_eqns thy tyco) - #-> (fn (thms, thm) => PureThy.note_thmss Thm.lemmaK + #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK [((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]), ((prefix tyco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])]) #> snd diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Sep 20 16:05:25 2010 +0200 @@ -334,7 +334,7 @@ (drop (length dt_names) inducts); in thy9 - |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []), + |> Global_Theory.add_thmss ([((prfx (Binding.name "simps"), simps), []), ((prfx (Binding.name "inducts"), inducts), []), ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []), ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites), @@ -367,7 +367,8 @@ |> store_thmss "inject" new_type_names raw_inject ||>> store_thmss "distinct" new_type_names raw_distinct ||> Sign.add_path (space_implode "_" new_type_names) - ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])] + ||>> Global_Theory.add_thms + [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])] ||> Sign.restore_naming thy1; in thy2 diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Sep 20 16:05:25 2010 +0200 @@ -122,7 +122,7 @@ val vs = map (fn i => List.nth (pnames, i)) is; val (thm', thy') = thy |> Sign.root_path - |> PureThy.store_thm + |> Global_Theory.store_thm (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm) ||> Sign.restore_naming thy; @@ -193,7 +193,7 @@ val exh_name = Thm.derivation_name exhaust; val (thm', thy') = thy |> Sign.root_path - |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm) + |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm) ||> Sign.restore_naming thy; val P = Var (("P", 0), rT' --> HOLogic.boolT); diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/Function/size.ML Mon Sep 20 16:05:25 2010 +0200 @@ -142,7 +142,7 @@ |> Sign.add_consts_i (map (fn (s, T) => (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn)) (size_names ~~ recTs1)) - |> PureThy.add_defs false + |> Global_Theory.add_defs false (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs))) (map Binding.name def_names ~~ (size_fns ~~ rec_combs1))) ||> Class.instantiation @@ -207,11 +207,12 @@ val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @ prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3; - val ([size_thms], thy'') = PureThy.add_thmss - [((Binding.name "size", size_eqns), - [Simplifier.simp_add, Nitpick_Simps.add, - Thm.declaration_attribute - (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy' + val ([size_thms], thy'') = + Global_Theory.add_thmss + [((Binding.name "size", size_eqns), + [Simplifier.simp_add, Nitpick_Simps.add, + Thm.declaration_attribute + (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'; in SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms)) diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Sep 20 16:05:25 2010 +0200 @@ -1303,7 +1303,7 @@ List.partition (is_typedef_axiom ctxt false) user_nondefs |>> append built_in_nondefs val defs = - (thy |> PureThy.all_thms_of + (thy |> Global_Theory.all_thms_of |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd) |> map (prop_of o snd) |> filter_out is_trivial_definition @@ -1867,7 +1867,7 @@ fun ground_theorem_table thy = fold ((fn @{const Trueprop} $ t1 => is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1) - | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty + | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy) Inttab.empty (* TODO: Move to "Nitpick.thy" *) val basic_ersatz_table = diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Sep 20 16:05:25 2010 +0200 @@ -2158,15 +2158,15 @@ val def = Logic.mk_equals (lhs, predterm) val ([definition], thy') = thy |> Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |> - PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])] + Global_Theory.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])] val ctxt' = ProofContext.init_global thy' val rules as ((intro, elim), _) = create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T)) in thy' |> set_function_name Pred name mode mode_cname |> add_predfun_data name mode (definition, rules) - |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd - |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd + |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd + |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd |> Theory.checkpoint end; in @@ -2883,7 +2883,7 @@ (fn thm => Context.mapping (Code.add_eqn thm) I)))) val thy''' = Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ => - fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss + fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [attrib thy ])] thy)) result_thms' thy'' |> Theory.checkpoint) diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Sep 20 16:05:25 2010 +0200 @@ -108,7 +108,7 @@ val def = Logic.mk_equals (lhs, atom) val ([definition], thy') = thy |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] - |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])] + |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])] in (lhs, ((full_constname, [definition]) :: defs, thy')) end @@ -327,7 +327,7 @@ val def = Logic.mk_equals (lhs, abs_arg') val ([definition], thy') = thy |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] - |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])] + |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])] in (list_comb (Logic.varify_global const, vars), ((full_constname, [definition])::new_defs, thy')) diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Sep 20 16:05:25 2010 +0200 @@ -57,7 +57,7 @@ val z3_rules_setup = Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #> - PureThy.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get) + Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get) end diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Sep 20 16:05:25 2010 +0200 @@ -708,7 +708,7 @@ fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths = let val thy = ProofContext.theory_of ctxt - val global_facts = PureThy.facts_of thy + val global_facts = Global_Theory.facts_of thy val local_facts = ProofContext.facts_of ctxt val named_locals = local_facts |> Facts.dest_static [] val assms = Assumption.all_assms_of ctxt diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Mon Sep 20 16:05:25 2010 +0200 @@ -382,7 +382,7 @@ $ functional val def_term = const_def thy (fid, Ty, wfrec_R_M) val ([def], thy') = - PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy + Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy in (thy', def) end; end; @@ -539,7 +539,7 @@ val defn = const_def thy (name, Ty, S.list_mk_abs (args,rhs)) val ([def0], theory) = thy - |> PureThy.add_defs false + |> Global_Theory.add_defs false [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)] val def = Thm.unvarify_global def0; val dummy = diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/choice_specification.ML Mon Sep 20 16:05:25 2010 +0200 @@ -33,7 +33,7 @@ else thname val def_eq = Logic.mk_equals (Const(cname_full,ctype), HOLogic.choice_const ctype $ P) - val (thms, thy') = PureThy.add_defs covld [((Binding.name cdefname, def_eq),[])] thy + val (thms, thy') = Global_Theory.add_defs covld [((Binding.name cdefname, def_eq),[])] thy val thm' = [thm,hd thms] MRS @{thm exE_some} in mk_definitional cos (thy',thm') @@ -189,7 +189,7 @@ if name = "" then arg |> Library.swap else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm); - PureThy.store_thm (Binding.name name, thm) thy) + Global_Theory.store_thm (Binding.name name, thm) thy) in args |> apsnd (remove_alls frees) |> apsnd undo_imps diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Mon Sep 20 16:05:25 2010 +0200 @@ -273,7 +273,7 @@ fun add_ind_realizer rsets intrs induct raw_induct elims vs thy = let val qualifier = Long_Name.qualifier (name_of_thm induct); - val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts"); + val inducts = Global_Theory.get_thms thy (Long_Name.qualify qualifier "inducts"); val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []); val ar = length vs + length iTs; val params = Inductive.params_of raw_induct; @@ -356,7 +356,7 @@ subst_atomic rlzpreds' (Logic.unvarify_global rintr))) (rintrs ~~ maps snd rss)) [] ||> Sign.root_path; - val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3'; + val thy3 = fold (Global_Theory.hide_fact false o name_of_thm) (#intrs ind_info) thy3'; (** realizer for induction rule **) @@ -395,11 +395,11 @@ REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' [K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac, DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); - val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_" + val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_" (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy; val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp))) (Datatype_Aux.split_conj_thm thm'); - val ([thms'], thy'') = PureThy.add_thmss + val ([thms'], thy'') = Global_Theory.add_thmss [((Binding.qualified_name (space_implode "_" (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @ ["correctness"])), thms), [])] thy'; @@ -454,7 +454,7 @@ rewrite_goals_tac rews, REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN' DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); - val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_" + val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_" (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy in Extraction.add_realizers_i diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/old_primrec.ML Mon Sep 20 16:05:25 2010 +0200 @@ -308,11 +308,11 @@ end; fun thy_note ((name, atts), thms) = - PureThy.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms)); + Global_Theory.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms)); fun thy_def false ((name, atts), t) = - PureThy.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm)) + Global_Theory.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm)) | thy_def true ((name, atts), t) = - PureThy.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm)); + Global_Theory.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm)); in diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/recdef.ML Mon Sep 20 16:05:25 2010 +0200 @@ -208,9 +208,9 @@ val ((simps' :: rules', [induct']), thy) = thy |> Sign.add_path bname - |> PureThy.add_thmss + |> Global_Theory.add_thmss (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) - ||>> PureThy.add_thms [((Binding.name "induct", induct), [])] + ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])] ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules); val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs}; val thy = @@ -239,7 +239,7 @@ val ([induct_rules'], thy3) = thy2 |> Sign.add_path bname - |> PureThy.add_thms [((Binding.name "induct_rules", induct_rules), [])] + |> Global_Theory.add_thms [((Binding.name "induct_rules", induct_rules), [])] ||> Sign.parent_path; in (thy3, {induct_rules = induct_rules'}) end; diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Tools/record.ML Mon Sep 20 16:05:25 2010 +0200 @@ -153,7 +153,7 @@ val ([isom_def], cdef_thy) = typ_thy |> Sign.declare_const ((isom_binding, isomT), NoSyn) |> snd - |> PureThy.add_defs false + |> Global_Theory.add_defs false [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])]; val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro)); @@ -1658,7 +1658,7 @@ fun mk_defs () = typ_thy |> Sign.declare_const ((ext_binding, ext_type), NoSyn) |> snd - |> PureThy.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])] + |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])] ||> Theory.checkpoint val ([ext_def], defs_thy) = timeit_msg "record extension constructor def:" mk_defs; @@ -1749,7 +1749,7 @@ val ([induct', inject', surjective', split_meta'], thm_thy) = defs_thy - |> PureThy.add_thms (map (Thm.no_attributes o apfst Binding.name) + |> Global_Theory.add_thms (map (Thm.no_attributes o apfst Binding.name) [("ext_induct", induct), ("ext_inject", inject), ("ext_surjective", surject), @@ -2096,11 +2096,12 @@ (sel_decls ~~ (field_syntax @ [NoSyn])) |> fold (fn (x, T) => snd o Sign.declare_const ((Binding.name x, T), NoSyn)) (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl]) - |> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) - sel_specs - ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) - upd_specs - ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) + |> (Global_Theory.add_defs false o + map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs + ||>> (Global_Theory.add_defs false o + map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs + ||>> (Global_Theory.add_defs false o + map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) [make_spec, fields_spec, extend_spec, truncate_spec] ||> Theory.checkpoint val (((sel_defs, upd_defs), derived_defs), defs_thy) = @@ -2339,7 +2340,7 @@ [surjective', equality']), [induct_scheme', induct', cases_scheme', cases']), thms_thy) = defs_thy - |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name)) + |> (Global_Theory.add_thmss o map (Thm.no_attributes o apfst Binding.name)) [("select_convs", sel_convs_standard), ("update_convs", upd_convs_standard), ("select_defs", sel_defs), @@ -2348,10 +2349,10 @@ ("unfold_congs", unfold_congs), ("splits", [split_meta_standard, split_object, split_ex]), ("defs", derived_defs)] - ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name)) + ||>> (Global_Theory.add_thms o map (Thm.no_attributes o apfst Binding.name)) [("surjective", surjective), ("equality", equality)] - ||>> (PureThy.add_thms o (map o apfst o apfst) Binding.name) + ||>> (Global_Theory.add_thms o (map o apfst o apfst) Binding.name) [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)), (("induct", induct), induct_type_global name), (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)), @@ -2364,7 +2365,7 @@ val ([simps', iffs'], thms_thy') = thms_thy - |> PureThy.add_thmss + |> Global_Theory.add_thmss [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]), ((Binding.name "iffs", iffs), [iff_add])]; diff -r 32a00ff29d1a -r fe5722fce758 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Mon Sep 20 16:05:25 2010 +0200 @@ -63,7 +63,7 @@ (Binding.suffix_name "_def" b, Logic.mk_equals (c, t)); val defs = map2 mk_def consts specs; val (def_thms, thy) = - PureThy.add_defs false (map Thm.no_attributes defs) thy; + Global_Theory.add_defs false (map Thm.no_attributes defs) thy; in ((consts, def_thms), thy) end; diff -r 32a00ff29d1a -r fe5722fce758 src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Mon Sep 20 16:05:25 2010 +0200 @@ -194,7 +194,7 @@ ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info; in theorems_thy - |> PureThy.add_thmss + |> Global_Theory.add_thmss [((Binding.qualified true "rews" comp_dbind, flat rewss @ take_rews), [])] |> snd diff -r 32a00ff29d1a -r fe5722fce758 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Sep 20 16:05:25 2010 +0200 @@ -169,7 +169,7 @@ (* register constant definitions *) val (fixdef_thms, thy) = - (PureThy.add_defs false o map Thm.no_attributes) + (Global_Theory.add_defs false o map Thm.no_attributes) (map (Binding.suffix_name "_def") binds ~~ eqns) thy; (* prove applied version of definitions *) @@ -201,7 +201,7 @@ (* register unfold theorems *) val (unfold_thms, thy) = - (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) + (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (mk_unfold_thms unfold_binds tuple_unfold_thm) thy; in ((proj_thms, unfold_thms), thy) @@ -242,13 +242,13 @@ val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy; val eqn = Logic.mk_equals (const, rhs); val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn); - val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy; + val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy; in ((const, def_thm), thy) end; fun add_qualified_thm name (dbind, thm) = - yield_singleton PureThy.add_thms + yield_singleton Global_Theory.add_thms ((Binding.qualified true name dbind, thm), []); (******************************************************************************) @@ -349,7 +349,7 @@ val deflation_map_binds = dbinds |> map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map"); val (deflation_map_thms, thy) = thy |> - (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) + (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (conjuncts deflation_map_binds deflation_map_thm); (* register map functions in theory data *) @@ -496,7 +496,7 @@ (* register REP equations *) val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dbinds; val (_, thy) = thy |> - (PureThy.add_thms o map Thm.no_attributes) + (Global_Theory.add_thms o map Thm.no_attributes) (REP_eq_binds ~~ REP_eq_thms); (* define rep/abs functions *) @@ -607,7 +607,7 @@ val thmR = thm RS @{thm conjunct2}; in (n, thmL):: conjuncts ns thmR end; val (isodefl_thms, thy) = thy |> - (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) + (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (conjuncts isodefl_binds isodefl_thm); val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy; @@ -631,7 +631,7 @@ map prove_map_ID_thm (map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms); val (_, thy) = thy |> - (PureThy.add_thms o map Thm.no_attributes) + (Global_Theory.add_thms o map Thm.no_attributes) (map_ID_binds ~~ map_ID_thms); val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy; diff -r 32a00ff29d1a -r fe5722fce758 src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Sep 20 16:05:25 2010 +0200 @@ -204,15 +204,15 @@ (******************************************************************************) fun add_qualified_def name (dbind, eqn) = - yield_singleton (PureThy.add_defs false) + yield_singleton (Global_Theory.add_defs false) ((Binding.qualified true name dbind, eqn), []); fun add_qualified_thm name (dbind, thm) = - yield_singleton PureThy.add_thms + yield_singleton Global_Theory.add_thms ((Binding.qualified true name dbind, thm), []); fun add_qualified_simp_thm name (dbind, thm) = - yield_singleton PureThy.add_thms + yield_singleton Global_Theory.add_thms ((Binding.qualified true name dbind, thm), [Simplifier.simp_add]); (******************************************************************************) diff -r 32a00ff29d1a -r fe5722fce758 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Sep 20 16:05:25 2010 +0200 @@ -124,7 +124,7 @@ val rep_const = #rep_const iso_info; local - fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); + fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s); in val ax_take_0 = ga "take_0" dname; val ax_take_strict = ga "take_strict" dname; @@ -200,7 +200,7 @@ in thy - |> PureThy.add_thmss [ + |> Global_Theory.add_thmss [ ((qualified "iso_rews" , iso_rews ), [simp]), ((qualified "nchotomy" , [nchotomy] ), []), ((qualified "exhaust" , [exhaust] ), @@ -240,8 +240,8 @@ val pg = pg' thy; local - fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); - fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s); + fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s); + fun gts s dn = Global_Theory.get_thms thy (dn ^ "." ^ s); in val axs_rep_iso = map (ga "rep_iso") dnames; val axs_abs_iso = map (ga "abs_iso") dnames; @@ -421,10 +421,10 @@ in thy - |> snd o PureThy.add_thmss [ + |> snd o Global_Theory.add_thmss [ ((Binding.qualified true "finite_induct" comp_dbind, [finite_ind]), []), ((Binding.qualified true "induct" comp_dbind, [ind] ), [])] - |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))) + |> (snd o Global_Theory.add_thmss (map ind_rule (dnames ~~ inducts))) end; (* prove_induction *) (******************************************************************************) @@ -444,7 +444,7 @@ val n_eqs = length eqs; val take_rews = - maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames; + maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames; (* ----- define bisimulation predicate -------------------------------------- *) @@ -465,7 +465,7 @@ singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t); fun legacy_infer_prop thy t = legacy_infer_term thy (Type.constraint propT t); fun infer_props thy = map (apsnd (legacy_infer_prop thy)); - fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x); + fun add_defs_i x = Global_Theory.add_defs false (map Thm.no_attributes x); fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; fun one_con (con, args) = @@ -568,7 +568,7 @@ in pg [] goal (K tacs) end; end; (* local *) -in thy |> snd o PureThy.add_thmss +in thy |> snd o Global_Theory.add_thmss [((Binding.qualified true "coinduct" comp_dbind, [coind]), [])] end; (* let *) @@ -603,7 +603,7 @@ val take_lemmas = #take_lemma_thms take_info; val take_rews = - maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames; + maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames; (* prove induction rules, unless definition is indirect recursive *) val thy = diff -r 32a00ff29d1a -r fe5722fce758 src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOLCF/Tools/fixrec.ML Mon Sep 20 16:05:25 2010 +0200 @@ -419,7 +419,7 @@ val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T)); val cname = case chead_of t of Const(c,_) => c | _ => fixrec_err "function is not declared as constant in theory"; - val unfold_thm = PureThy.get_thm thy (cname^".unfold"); + val unfold_thm = Global_Theory.get_thm thy (cname^".unfold"); val simp = Goal.prove_global thy [] [] eq (fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]); in simp end; @@ -431,7 +431,7 @@ val ts = map (prep_term thy) strings; val simps = map (fix_pat thy) ts; in - (snd o PureThy.add_thmss [((name, simps), atts)]) thy + (snd o Global_Theory.add_thmss [((name, simps), atts)]) thy end; val add_fixpat = gen_add_fixpat Sign.cert_term (K I); diff -r 32a00ff29d1a -r fe5722fce758 src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOLCF/Tools/pcpodef.ML Mon Sep 20 16:05:25 2010 +0200 @@ -100,7 +100,7 @@ val (_, thy) = thy |> Sign.add_path (Binding.name_of name) - |> PureThy.add_thms + |> Global_Theory.add_thms ([((Binding.prefix_name "adm_" name, admissible'), []), ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), @@ -143,7 +143,7 @@ val (_, thy) = thy |> Sign.add_path (Binding.name_of name) - |> PureThy.add_thms + |> Global_Theory.add_thms ([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []), ((Binding.suffix_name "_strict" Abs_name, Abs_strict), []), ((Binding.suffix_name "_strict_iff" Rep_name, Rep_strict_iff), []), diff -r 32a00ff29d1a -r fe5722fce758 src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOLCF/Tools/repdef.ML Mon Sep 20 16:05:25 2010 +0200 @@ -139,7 +139,7 @@ [type_definition_thm, #below_def cpo_info, emb_def, prj_def]; val (REP_thm, thy) = thy |> Sign.add_path (Binding.name_of name) - |> PureThy.add_thm + |> Global_Theory.add_thm ((Binding.prefix_name "REP_" name, Drule.zero_var_indexes (@{thm typedef_REP} OF typedef_thms')), []) ||> Sign.restore_naming thy; diff -r 32a00ff29d1a -r fe5722fce758 src/HOLCF/ex/Pattern_Match.thy --- a/src/HOLCF/ex/Pattern_Match.thy Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOLCF/ex/Pattern_Match.thy Mon Sep 20 16:05:25 2010 +0200 @@ -379,7 +379,7 @@ (Binding.suffix_name "_def" b, Logic.mk_equals (c, t)); val defs = map2 mk_def consts specs; val (def_thms, thy) = - PureThy.add_defs false (map Thm.no_attributes defs) thy; + Global_Theory.add_defs false (map Thm.no_attributes defs) thy; in ((consts, def_thms), thy) end; diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/IsaMakefile Mon Sep 20 16:05:25 2010 +0200 @@ -218,6 +218,7 @@ drule.ML \ envir.ML \ facts.ML \ + global_theory.ML \ goal.ML \ goal_display.ML \ interpretation.ML \ diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/attrib.ML Mon Sep 20 16:05:25 2010 +0200 @@ -181,7 +181,7 @@ fun gen_thm pick = Scan.depend (fn context => let val thy = Context.theory_of context; - val get = Context.cases (PureThy.get_fact context) ProofContext.get_fact context; + val get = Context.cases (Global_Theory.get_fact context) ProofContext.get_fact context; val get_fact = get o Facts.Fact; fun get_named pos name = get (Facts.Named ((name, pos), NONE)); in diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/calculation.ML Mon Sep 20 16:05:25 2010 +0200 @@ -98,7 +98,7 @@ "declaration of symmetry rule" #> Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric) "resolution with symmetry rule" #> - PureThy.add_thms + Global_Theory.add_thms [((Binding.empty, transitive_thm), [trans_add]), ((Binding.empty, symmetric_thm), [sym_add])] #> snd)); diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/class.ML Mon Sep 20 16:05:25 2010 +0200 @@ -329,7 +329,7 @@ |> snd |> Thm.add_def false false (b_def, def_eq) |>> apsnd Thm.varifyT_global - |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm) + |-> (fn (_, def_thm) => Global_Theory.store_thm (b_def, def_thm) #> snd #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm)))) |> Sign.add_const_constraint (c', SOME ty') diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/context_rules.ML Mon Sep 20 16:05:25 2010 +0200 @@ -196,7 +196,7 @@ val dest_query = rule_add elim_queryK Tactic.make_elim; val _ = Context.>> (Context.map_theory - (snd o PureThy.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])])); + (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])])); (* concrete syntax *) diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/element.ML Mon Sep 20 16:05:25 2010 +0200 @@ -480,7 +480,7 @@ val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts; in context |> Context.mapping_result - (PureThy.note_thmss kind facts') + (Global_Theory.note_thmss kind facts') (ProofContext.note_thmss kind facts') end; diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/expression.ML Mon Sep 20 16:05:25 2010 +0200 @@ -640,7 +640,7 @@ thy |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], []) |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd - |> PureThy.add_defs false + |> Global_Theory.add_defs false [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])]; val defs_ctxt = ProofContext.init_global defs_thy |> Variable.declare_term head; @@ -681,7 +681,7 @@ val (_, thy'') = thy' |> Sign.qualified_path true abinding - |> PureThy.note_thmss "" + |> Global_Theory.note_thmss "" [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])] ||> Sign.restore_naming thy'; in (SOME statement, SOME intro, axioms, thy'') end; @@ -695,7 +695,7 @@ val (_, thy'''') = thy''' |> Sign.qualified_path true binding - |> PureThy.note_thmss "" + |> Global_Theory.note_thmss "" [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]), ((Binding.conceal (Binding.name axiomsN), []), [(map (Drule.export_without_context o Element.conclude_witness) axioms, [])])] diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/generic_target.ML Mon Sep 20 16:05:25 2010 +0200 @@ -122,7 +122,7 @@ |> Drule.zero_var_indexes_list; (*thm definition*) - val result = PureThy.name_thm true true name th''; + val result = Global_Theory.name_thm true true name th''; (*import fixes*) val (tvars, vars) = @@ -142,7 +142,7 @@ NONE => raise THM ("Failed to re-import result", 0, [result']) | SOME res => Local_Defs.contract ctxt defs (Thm.cprop_of th) res) |> Goal.norm_result - |> PureThy.name_thm false false name; + |> Global_Theory.name_thm false false name; in (result'', result) end; @@ -150,11 +150,11 @@ let val thy = ProofContext.theory_of lthy; val facts' = facts - |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi + |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi (Local_Theory.full_name lthy (fst a))) bs)) - |> PureThy.map_facts (import_export_proof lthy); - val local_facts = PureThy.map_facts #1 facts'; - val global_facts = PureThy.map_facts #2 facts'; + |> Global_Theory.map_facts (import_export_proof lthy); + val local_facts = Global_Theory.map_facts #1 facts'; + val global_facts = Global_Theory.map_facts #2 facts'; in lthy |> target_notes kind global_facts local_facts @@ -214,7 +214,7 @@ val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts; in lthy - |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd) + |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd) |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd) end; diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Mon Sep 20 16:05:25 2010 +0200 @@ -174,8 +174,9 @@ val add_axioms = fold (snd oo Specification.axiom_cmd); fun add_defs ((unchecked, overloaded), args) thy = - thy |> (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded - (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args) + thy |> + (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd) + overloaded (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args) |> snd; @@ -215,7 +216,8 @@ val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class; val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type; val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const; -val hide_fact = hide_names PureThy.intern_fact PureThy.defined_fact PureThy.hide_fact; +val hide_fact = + hide_names Global_Theory.intern_fact Global_Theory.defined_fact Global_Theory.hide_fact; (* goals *) diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/locale.ML Mon Sep 20 16:05:25 2010 +0200 @@ -506,7 +506,7 @@ let val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |> Attrib.map_facts (Attrib.attribute_i thy) - in PureThy.note_thmss kind args'' #> snd end) + in Global_Theory.note_thmss kind args'' #> snd end) (registrations_of (Context.Theory thy) loc) thy)) in ctxt'' end; diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/named_target.ML Mon Sep 20 16:05:25 2010 +0200 @@ -118,7 +118,7 @@ (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts; in lthy - |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd) + |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd) |> Local_Theory.target (Locale.add_thmss locale kind local_facts') end diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Mon Sep 20 16:05:25 2010 +0200 @@ -297,7 +297,7 @@ fun extern_fact ctxt name = let val local_facts = facts_of ctxt; - val global_facts = PureThy.facts_of (theory_of ctxt); + val global_facts = Global_Theory.facts_of (theory_of ctxt); in if is_some (Facts.lookup (Context.Proof ctxt) local_facts name) then Facts.extern local_facts name @@ -790,7 +790,7 @@ extern_const = Consts.extern consts}; in Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt - (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax (theory_of ctxt))) + (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (theory_of ctxt))) end; in @@ -982,7 +982,7 @@ SOME (_, ths) => (Context_Position.report ctxt pos (Markup.local_fact name); map (Thm.transfer thy) (Facts.select thmref ths)) - | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref); + | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref); in pick name thms end; in @@ -1012,12 +1012,12 @@ val name = full_name ctxt b; val _ = Context_Position.report ctxt pos (Markup.local_fact_decl name); - val facts = PureThy.name_thmss false name raw_facts; + val facts = Global_Theory.name_thmss false name raw_facts; fun app (th, attrs) x = swap (Library.foldl_map (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th)); val (res, ctxt') = fold_map app facts ctxt; - val thms = PureThy.name_thms false false name (flat res); + val thms = Global_Theory.name_thms false false name (flat res); val Mode {stmt, ...} = get_mode ctxt; in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end); diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/proof_display.ML Mon Sep 20 16:05:25 2010 +0200 @@ -49,9 +49,9 @@ fun pretty_theorems_diff verbose prev_thys thy = let val pretty_fact = ProofContext.pretty_fact (ProofContext.init_global thy); - val facts = PureThy.facts_of thy; + val facts = Global_Theory.facts_of thy; val thmss = - Facts.dest_static (map PureThy.facts_of prev_thys) facts + Facts.dest_static (map Global_Theory.facts_of prev_thys) facts |> not verbose ? filter_out (Facts.is_concealed facts o #1); in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end; diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Isar/specification.ML Mon Sep 20 16:05:25 2010 +0200 @@ -180,7 +180,7 @@ val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) => fold_map Thm.add_axiom (map (apfst (fn a => Binding.map_name (K a) b)) - (PureThy.name_multi (Name.of_binding b) (map subst props))) + (Global_Theory.name_multi (Name.of_binding b) (map subst props))) #>> (fn ths => ((b, atts), [(map #2 ths, [])]))); (*facts*) diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/ML/ml_context.ML Mon Sep 20 16:05:25 2010 +0200 @@ -75,7 +75,7 @@ fun ml_store get (name, ths) = let val ths' = Context.>>> (Context.map_theory_result - (PureThy.store_thms (Binding.name name, ths))); + (Global_Theory.store_thms (Binding.name name, ths))); val _ = Context.>> (Context.map_theory (Stored_Thms.put ths')); val _ = if name = "" then () diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Proof/extraction.ML Mon Sep 20 16:05:25 2010 +0200 @@ -783,11 +783,11 @@ val (def_thms, thy') = if t = nullt then ([], thy) else thy |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)] - |> PureThy.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"), + |> Global_Theory.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"), Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])] in thy' - |> PureThy.store_thm (Binding.qualified_name (corr_name s vs), + |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs), Thm.varifyT_global (funpow (length (vars_of corr_prop)) (Thm.forall_elim_var 0) (Thm.forall_intr_frees (ProofChecker.thm_of_proof thy' @@ -815,7 +815,7 @@ Keyword.thy_decl (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >> (fn xs => Toplevel.theory (fn thy => add_realizers - (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy))); + (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy))); val _ = Outer_Syntax.command "realizability" @@ -830,7 +830,7 @@ val _ = Outer_Syntax.command "extract" "extract terms from proofs" Keyword.thy_decl (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy => - extract (map (apfst (PureThy.get_thm thy)) xs) thy))); + extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); val etype_of = etype_of o add_syntax; diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Mon Sep 20 16:05:25 2010 +0200 @@ -88,7 +88,7 @@ fun proof_of_term thy ty = let - val thms = PureThy.all_thms_of thy; + val thms = Global_Theory.all_thms_of thy; val axms = Theory.all_axioms_of thy; fun mk_term t = (if ty then I else map_types (K dummyT)) @@ -188,7 +188,7 @@ fun cterm_of_proof thy prf = let - val thm_names = map fst (PureThy.all_thms_of thy); + val thm_names = map fst (Global_Theory.all_thms_of thy); val axm_names = map fst (Theory.all_axioms_of thy); val thy' = thy |> add_proof_syntax @@ -207,7 +207,7 @@ fun read_term thy topsort = let - val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy)); + val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy)); val axm_names = map fst (Theory.all_axioms_of thy); val ctxt = thy |> add_proof_syntax diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Proof/proofchecker.ML --- a/src/Pure/Proof/proofchecker.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Proof/proofchecker.ML Mon Sep 20 16:05:25 2010 +0200 @@ -16,7 +16,7 @@ (***** construct a theorem out of a proof term *****) fun lookup_thm thy = - let val tab = fold_rev Symtab.update (PureThy.all_thms_of thy) Symtab.empty + let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in (fn s => case Symtab.lookup tab s of NONE => error ("Unknown theorem " ^ quote s) diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Sep 20 16:05:25 2010 +0200 @@ -267,8 +267,8 @@ fun new_thms_deps thy thy' = let - val prev_facts = PureThy.facts_of thy; - val facts = PureThy.facts_of thy'; + val prev_facts = Global_Theory.facts_of thy; + val facts = Global_Theory.facts_of thy'; in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end; end; @@ -519,7 +519,7 @@ fun theory_facts name = let val thy = Thy_Info.get_theory name - in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end; + in (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy) end; fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static); fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static); @@ -608,7 +608,7 @@ What we want is mapping onto simple PGIP name/context model. *) val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *) val thy = ProofContext.theory_of ctx - val ths = [PureThy.get_thm thy thmname] + val ths = [Global_Theory.get_thm thy thmname] val deps = #2 (thms_deps ths); in if null deps then () @@ -649,7 +649,7 @@ text=[XML.Elem (("pgml", []), maps YXML.parse_body strings)] }) fun strings_of_thm (thy, name) = - map (Display.string_of_thm_global thy) (PureThy.get_thms thy name) + map (Display.string_of_thm_global thy) (Global_Theory.get_thms thy name) val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false in diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/ROOT.ML Mon Sep 20 16:05:25 2010 +0200 @@ -134,6 +134,7 @@ use "thm.ML"; use "more_thm.ML"; use "facts.ML"; +use "global_theory.ML"; use "pure_thy.ML"; use "drule.ML"; use "morphism.ML"; diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Thy/thm_deps.ML Mon Sep 20 16:05:25 2010 +0200 @@ -49,7 +49,7 @@ fun unused_thms (base_thys, thys) = let fun add_fact space (name, ths) = - if exists (fn thy => PureThy.defined_fact thy name) base_thys then I + if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I else let val {concealed, group, ...} = Name_Space.the_entry space name in fold_rev (fn th => @@ -60,7 +60,7 @@ fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts; val new_thms = - fold (add_facts o PureThy.facts_of) thys [] + fold (add_facts o Global_Theory.facts_of) thys [] |> sort_distinct (string_ord o pairself #1); val used = diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Thy/thy_info.ML Mon Sep 20 16:05:25 2010 +0200 @@ -194,7 +194,7 @@ tasks |> maps (fn name => let val (thy, after_load) = Future.join (the (Symtab.lookup futures name)); - val _ = PureThy.join_proofs thy; + val _ = Global_Theory.join_proofs thy; val _ = after_load (); in [] end handle exn => [Exn.Exn exn]) |> rev |> Exn.release_all; diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Tools/find_theorems.ML Mon Sep 20 16:05:25 2010 +0200 @@ -350,7 +350,7 @@ fun nicer_shortest ctxt = let (* FIXME global name space!? *) - val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt)); + val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt)); val shorten = Name_Space.extern_flags @@ -381,7 +381,7 @@ |> filter_out (Facts.is_concealed facts o #1); in maps Facts.selections - (visible_facts (PureThy.facts_of (ProofContext.theory_of ctxt)) @ + (visible_facts (Global_Theory.facts_of (ProofContext.theory_of ctxt)) @ visible_facts (ProofContext.facts_of ctxt)) end; diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/Tools/named_thms.ML --- a/src/Pure/Tools/named_thms.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/Tools/named_thms.ML Mon Sep 20 16:05:25 2010 +0200 @@ -39,6 +39,6 @@ val setup = Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #> - PureThy.add_thms_dynamic (Binding.name name, content); + Global_Theory.add_thms_dynamic (Binding.name name, content); end; diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/assumption.ML --- a/src/Pure/assumption.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/assumption.ML Mon Sep 20 16:05:25 2010 +0200 @@ -81,7 +81,7 @@ (*named prems -- legacy feature*) val _ = Context.>> - (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems", + (Context.map_theory (Global_Theory.add_thms_dynamic (Binding.name "prems", fn Context.Theory _ => [] | Context.Proof ctxt => all_prems_of ctxt))); diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/axclass.ML Mon Sep 20 16:05:25 2010 +0200 @@ -390,7 +390,7 @@ (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const')) #>> apsnd Thm.varifyT_global #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm) - #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), []) + #> Global_Theory.add_thm ((Binding.conceal (Binding.name c'), thm), []) #> #2 #> pair (Const (c, T)))) ||> Sign.restore_naming thy @@ -419,7 +419,7 @@ fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); val rel = Logic.dest_classrel prop handle TERM _ => err (); val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); - val (th', thy') = PureThy.store_thm + val (th', thy') = Global_Theory.store_thm (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy; val th'' = th' |> Thm.unconstrainT @@ -438,7 +438,7 @@ fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); - val (th', thy') = PureThy.store_thm + val (th', thy') = Global_Theory.store_thm (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy; val args = Name.names Name.context Name.aT Ss; @@ -560,7 +560,7 @@ val ([def], def_thy) = thy |> Sign.primitive_class (bclass, super) - |> PureThy.add_defs false [((Thm.def_binding bconst, class_eq), [])]; + |> Global_Theory.add_defs false [((Thm.def_binding bconst, class_eq), [])]; val (raw_intro, (raw_classrel, raw_axioms)) = split_defined (length conjs) def ||> chop (length super); @@ -571,7 +571,7 @@ val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) = def_thy |> Sign.qualified_path true bconst - |> PureThy.note_thmss "" + |> Global_Theory.note_thmss "" [((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]), ((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]), ((Binding.name "axioms", []), @@ -586,7 +586,8 @@ facts_thy |> fold (#2 oo put_trancl_classrel) (map (pair class) super ~~ classrel) |> Sign.qualified_path false bconst - |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> #2 + |> Global_Theory.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) + |> #2 |> Sign.restore_naming facts_thy |> map_axclasses (Symtab.update (class, axclass)) |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params); diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/drule.ML --- a/src/Pure/drule.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/drule.ML Mon Sep 20 16:05:25 2010 +0200 @@ -433,10 +433,10 @@ val read_prop = certify o Simple_Syntax.read_prop; fun store_thm name th = - Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th))); + Context.>>> (Context.map_theory_result (Global_Theory.store_thm (name, th))); fun store_thm_open name th = - Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th))); + Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th))); fun store_standard_thm name th = store_thm name (export_without_context th); fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm); diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/global_theory.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/global_theory.ML Mon Sep 20 16:05:25 2010 +0200 @@ -0,0 +1,224 @@ +(* Title: Pure/global_theory.ML + Author: Makarius + +Global theory content: stored facts. +*) + +signature GLOBAL_THEORY = +sig + val facts_of: theory -> Facts.T + val intern_fact: theory -> xstring -> string + val defined_fact: theory -> string -> bool + val hide_fact: bool -> string -> theory -> theory + val join_proofs: theory -> unit + val get_fact: Context.generic -> theory -> Facts.ref -> thm list + val get_thms: theory -> xstring -> thm list + val get_thm: theory -> xstring -> thm + val all_thms_of: theory -> (string * thm) list + val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list + val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list + val burrow_facts: ('a list -> 'b list) -> + ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list + val name_multi: string -> 'a list -> (string * 'a) list + val name_thm: bool -> bool -> string -> thm -> thm + val name_thms: bool -> bool -> string -> thm list -> thm list + val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list + val store_thms: binding * thm list -> theory -> thm list * theory + val store_thm: binding * thm -> theory -> thm * theory + val store_thm_open: binding * thm -> theory -> thm * theory + val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory + val add_thm: (binding * thm) * attribute list -> theory -> thm * theory + val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory + val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory + val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list + -> theory -> (string * thm list) list * theory + val add_defs: bool -> ((binding * term) * attribute list) list -> + theory -> thm list * theory + val add_defs_unchecked: bool -> ((binding * term) * attribute list) list -> + theory -> thm list * theory + val add_defs_cmd: bool -> ((binding * string) * attribute list) list -> + theory -> thm list * theory + val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list -> + theory -> thm list * theory +end; + +structure Global_Theory: GLOBAL_THEORY = +struct + +(** theory data **) + +structure Data = Theory_Data +( + type T = Facts.T * thm list; + val empty = (Facts.empty, []); + fun extend (facts, _) = (facts, []); + fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []); +); + + +(* facts *) + +val facts_of = #1 o Data.get; + +val intern_fact = Facts.intern o facts_of; +val defined_fact = Facts.defined o facts_of; + +fun hide_fact fully name = Data.map (apfst (Facts.hide fully name)); + + +(* proofs *) + +fun register_proofs (thy, thms) = (Data.map (apsnd (append thms)) thy, thms); + +fun join_proofs thy = Thm.join_proofs (rev (#2 (Data.get thy))); + + + +(** retrieve theorems **) + +fun get_fact context thy xthmref = + let + val xname = Facts.name_of_ref xthmref; + val pos = Facts.pos_of_ref xthmref; + + val name = intern_fact thy xname; + val res = Facts.lookup context (facts_of thy) name; + val _ = Theory.check_thy thy; + in + (case res of + NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos) + | SOME (static, ths) => + (Position.report pos ((if static then Markup.fact else Markup.dynamic_fact) name); + Facts.select xthmref (map (Thm.transfer thy) ths))) + end; + +fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named; +fun get_thm thy name = Facts.the_single name (get_thms thy name); + +fun all_thms_of thy = + Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) []; + + + +(** store theorems **) + +(* fact specifications *) + +fun map_facts f = map (apsnd (map (apfst (map f)))); +fun burrow_fact f = split_list #>> burrow f #> op ~~; +fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~; + + +(* naming *) + +fun name_multi name [x] = [(name, x)] + | name_multi "" xs = map (pair "") xs + | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; + +fun name_thm pre official name thm = thm + |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name + |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name); + +fun name_thms pre official name xs = + map (uncurry (name_thm pre official)) (name_multi name xs); + +fun name_thmss official name fact = + burrow_fact (name_thms true official name) fact; + + +(* enter_thms *) + +fun enter_thms pre_name post_name app_att (b, thms) thy = + if Binding.is_empty b + then swap (register_proofs (app_att (thy, thms))) + else + let + val naming = Sign.naming_of thy; + val name = Name_Space.full_name naming b; + val (thy', thms') = + register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms))); + val thms'' = map (Thm.transfer thy') thms'; + val thy'' = thy' |> (Data.map o apfst) (Facts.add_global naming (b, thms'') #> snd); + in (thms'', thy'') end; + + +(* store_thm(s) *) + +fun store_thms (b, thms) = + enter_thms (name_thms true true) (name_thms false true) I (b, thms); + +fun store_thm (b, th) = store_thms (b, [th]) #>> the_single; + +fun store_thm_open (b, th) = + enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single; + + +(* add_thms(s) *) + +fun add_thms_atts pre_name ((b, thms), atts) = + enter_thms pre_name (name_thms false true) + (Library.foldl_map (Thm.theory_attributes atts)) (b, thms); + +fun gen_add_thmss pre_name = + fold_map (add_thms_atts pre_name); + +fun gen_add_thms pre_name args = + apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args); + +val add_thmss = gen_add_thmss (name_thms true true); +val add_thms = gen_add_thms (name_thms true true); +val add_thm = yield_singleton add_thms; + + +(* add_thms_dynamic *) + +fun add_thms_dynamic (b, f) thy = thy + |> (Data.map o apfst) + (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd); + + +(* note_thmss *) + +fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy => + let + val pos = Binding.pos_of b; + val name = Sign.full_name thy b; + val _ = Position.report pos (Markup.fact_decl name); + + fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths); + val (thms, thy') = thy |> enter_thms + (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app) + (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts); + in ((name, thms), thy') end); + + +(* store axioms as theorems *) + +local + +fun no_read _ (_, t) = t; + +fun read thy (b, str) = + Syntax.read_prop_global thy str handle ERROR msg => + cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b)); + +fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy => + let + val prop = prep thy (b, raw_prop); + val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy; + val thm = def + |> Thm.forall_intr_frees + |> Thm.forall_elim_vars 0 + |> Thm.varifyT_global; + in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end); + +in + +val add_defs = add no_read false; +val add_defs_unchecked = add no_read true; +val add_defs_cmd = add read false; +val add_defs_unchecked_cmd = add read true; + +end; + +end; diff -r 32a00ff29d1a -r fe5722fce758 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Pure/pure_thy.ML Mon Sep 20 16:05:25 2010 +0200 @@ -1,235 +1,18 @@ (* Title: Pure/pure_thy.ML Author: Markus Wenzel, TU Muenchen -Theorem storage. Pure theory syntax and logical content. +Pure theory syntax and further logical content. *) signature PURE_THY = sig - val facts_of: theory -> Facts.T - val intern_fact: theory -> xstring -> string - val defined_fact: theory -> string -> bool - val hide_fact: bool -> string -> theory -> theory - val join_proofs: theory -> unit - val get_fact: Context.generic -> theory -> Facts.ref -> thm list - val get_thms: theory -> xstring -> thm list - val get_thm: theory -> xstring -> thm - val all_thms_of: theory -> (string * thm) list - val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list - val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list - val burrow_facts: ('a list -> 'b list) -> - ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list - val name_multi: string -> 'a list -> (string * 'a) list - val name_thm: bool -> bool -> string -> thm -> thm - val name_thms: bool -> bool -> string -> thm list -> thm list - val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list - val store_thms: binding * thm list -> theory -> thm list * theory - val store_thm: binding * thm -> theory -> thm * theory - val store_thm_open: binding * thm -> theory -> thm * theory - val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory - val add_thm: (binding * thm) * attribute list -> theory -> thm * theory - val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory - val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory - val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list - -> theory -> (string * thm list) list * theory - val add_defs: bool -> ((binding * term) * attribute list) list -> - theory -> thm list * theory - val add_defs_unchecked: bool -> ((binding * term) * attribute list) list -> - theory -> thm list * theory - val add_defs_cmd: bool -> ((binding * string) * attribute list) list -> - theory -> thm list * theory - val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list -> - theory -> thm list * theory val old_appl_syntax: theory -> bool val old_appl_syntax_setup: theory -> theory end; -structure PureThy: PURE_THY = +structure Pure_Thy: PURE_THY = struct - -(*** stored facts ***) - -(** theory data **) - -structure Global_Facts = Theory_Data -( - type T = Facts.T * thm list; - val empty = (Facts.empty, []); - fun extend (facts, _) = (facts, []); - fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []); -); - - -(* facts *) - -val facts_of = #1 o Global_Facts.get; - -val intern_fact = Facts.intern o facts_of; -val defined_fact = Facts.defined o facts_of; - -fun hide_fact fully name = Global_Facts.map (apfst (Facts.hide fully name)); - - -(* proofs *) - -fun register_proofs (thy, thms) = (Global_Facts.map (apsnd (append thms)) thy, thms); - -fun join_proofs thy = Thm.join_proofs (rev (#2 (Global_Facts.get thy))); - - - -(** retrieve theorems **) - -fun get_fact context thy xthmref = - let - val xname = Facts.name_of_ref xthmref; - val pos = Facts.pos_of_ref xthmref; - - val name = intern_fact thy xname; - val res = Facts.lookup context (facts_of thy) name; - val _ = Theory.check_thy thy; - in - (case res of - NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos) - | SOME (static, ths) => - (Position.report pos ((if static then Markup.fact else Markup.dynamic_fact) name); - Facts.select xthmref (map (Thm.transfer thy) ths))) - end; - -fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named; -fun get_thm thy name = Facts.the_single name (get_thms thy name); - -fun all_thms_of thy = - Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) []; - - - -(** store theorems **) - -(* fact specifications *) - -fun map_facts f = map (apsnd (map (apfst (map f)))); -fun burrow_fact f = split_list #>> burrow f #> op ~~; -fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~; - - -(* naming *) - -fun name_multi name [x] = [(name, x)] - | name_multi "" xs = map (pair "") xs - | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; - -fun name_thm pre official name thm = thm - |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name - |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name); - -fun name_thms pre official name xs = - map (uncurry (name_thm pre official)) (name_multi name xs); - -fun name_thmss official name fact = - burrow_fact (name_thms true official name) fact; - - -(* enter_thms *) - -fun enter_thms pre_name post_name app_att (b, thms) thy = - if Binding.is_empty b - then swap (register_proofs (app_att (thy, thms))) - else - let - val naming = Sign.naming_of thy; - val name = Name_Space.full_name naming b; - val (thy', thms') = - register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms))); - val thms'' = map (Thm.transfer thy') thms'; - val thy'' = thy' |> (Global_Facts.map o apfst) (Facts.add_global naming (b, thms'') #> snd); - in (thms'', thy'') end; - - -(* store_thm(s) *) - -fun store_thms (b, thms) = - enter_thms (name_thms true true) (name_thms false true) I (b, thms); - -fun store_thm (b, th) = store_thms (b, [th]) #>> the_single; - -fun store_thm_open (b, th) = - enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single; - - -(* add_thms(s) *) - -fun add_thms_atts pre_name ((b, thms), atts) = - enter_thms pre_name (name_thms false true) - (Library.foldl_map (Thm.theory_attributes atts)) (b, thms); - -fun gen_add_thmss pre_name = - fold_map (add_thms_atts pre_name); - -fun gen_add_thms pre_name args = - apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args); - -val add_thmss = gen_add_thmss (name_thms true true); -val add_thms = gen_add_thms (name_thms true true); -val add_thm = yield_singleton add_thms; - - -(* add_thms_dynamic *) - -fun add_thms_dynamic (b, f) thy = thy - |> (Global_Facts.map o apfst) - (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd); - - -(* note_thmss *) - -fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy => - let - val pos = Binding.pos_of b; - val name = Sign.full_name thy b; - val _ = Position.report pos (Markup.fact_decl name); - - fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths); - val (thms, thy') = thy |> enter_thms - (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app) - (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts); - in ((name, thms), thy') end); - - -(* store axioms as theorems *) - -local - -fun no_read _ (_, t) = t; - -fun read thy (b, str) = - Syntax.read_prop_global thy str handle ERROR msg => - cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b)); - -fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy => - let - val prop = prep thy (b, raw_prop); - val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy; - val thm = def - |> Thm.forall_intr_frees - |> Thm.forall_elim_vars 0 - |> Thm.varifyT_global; - in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end); - -in - -val add_defs = add no_read false; -val add_defs_unchecked = add no_read true; -val add_defs_cmd = add read false; -val add_defs_unchecked_cmd = add read true; - -end; - - - -(*** Pure theory syntax and logical content ***) - val typ = Simple_Syntax.read_typ; val prop = Simple_Syntax.read_prop; @@ -366,7 +149,7 @@ [(Binding.name "term", typ "'a => prop", NoSyn), (Binding.name "sort_constraint", typ "'a itself => prop", NoSyn), (Binding.name "conjunction", typ "prop => prop => prop", NoSyn)] - #> (add_defs false o map Thm.no_attributes) + #> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"), (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"), (Binding.name "sort_constraint_def", @@ -376,7 +159,7 @@ #> Sign.hide_const false "Pure.term" #> Sign.hide_const false "Pure.sort_constraint" #> Sign.hide_const false "Pure.conjunction" - #> add_thmss [((Binding.name "nothing", []), [])] #> snd + #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd #> fold (fn (a, prop) => snd o Thm.add_axiom (Binding.name a, prop)) Proofterm.equality_axms)); end; diff -r 32a00ff29d1a -r fe5722fce758 src/Sequents/Sequents.thy --- a/src/Sequents/Sequents.thy Mon Sep 20 15:29:53 2010 +0200 +++ b/src/Sequents/Sequents.thy Mon Sep 20 16:05:25 2010 +0200 @@ -10,7 +10,7 @@ uses ("prover.ML") begin -setup PureThy.old_appl_syntax_setup +setup Pure_Thy.old_appl_syntax_setup declare [[unify_trace_bound = 20, unify_search_bound = 40]] diff -r 32a00ff29d1a -r fe5722fce758 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/ZF/Tools/datatype_package.ML Mon Sep 20 16:05:25 2010 +0200 @@ -242,17 +242,18 @@ val need_recursor = (not coind andalso recursor_typ <> case_typ); fun add_recursor thy = - if need_recursor then - thy |> Sign.add_consts_i - [(Binding.name recursor_base_name, recursor_typ, NoSyn)] - |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def]) - else thy; + if need_recursor then + thy + |> Sign.add_consts_i + [(Binding.name recursor_base_name, recursor_typ, NoSyn)] + |> (snd o Global_Theory.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def]) + else thy; val (con_defs, thy0) = thy_path |> Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists))) - |> PureThy.add_defs false + |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) (case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)))) @@ -379,7 +380,7 @@ in (*Updating theory components: simprules and datatype info*) (thy1 |> Sign.add_path big_rec_base_name - |> PureThy.add_thmss + |> Global_Theory.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add]), ((Binding.empty , intrs), [Classical.safe_intro NONE]), ((Binding.name "con_defs", con_defs), []), diff -r 32a00ff29d1a -r fe5722fce758 src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/ZF/Tools/ind_cases.ML Mon Sep 20 16:05:25 2010 +0200 @@ -50,7 +50,7 @@ val facts = args |> map (fn ((name, srcs), props) => ((name, map (Attrib.attribute thy) srcs), map (Thm.no_attributes o single o smart_cases ctxt) props)); - in thy |> PureThy.note_thmss "" facts |> snd end; + in thy |> Global_Theory.note_thmss "" facts |> snd end; (* ind_cases method *) diff -r 32a00ff29d1a -r fe5722fce758 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/ZF/Tools/induct_tacs.ML Mon Sep 20 16:05:25 2010 +0200 @@ -158,7 +158,7 @@ in thy |> Sign.add_path (Long_Name.base_name big_rec_name) - |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd + |> Global_Theory.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy)) |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy)) |> Sign.parent_path diff -r 32a00ff29d1a -r fe5722fce758 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/ZF/Tools/inductive_package.ML Mon Sep 20 16:05:25 2010 +0200 @@ -172,7 +172,7 @@ val (_, thy1) = thy |> Sign.add_path big_rec_base_name - |> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs); + |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs); val ctxt1 = ProofContext.init_global thy1; @@ -508,7 +508,7 @@ val ([induct', mutual_induct'], thy') = thy - |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), induct), + |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), induct), [case_names, Induct.induct_pred big_rec_name]), ((Binding.name "mutual_induct", mutual_induct), [case_names])]; in ((thy', induct'), mutual_induct') @@ -520,7 +520,7 @@ if not coind then induction_rules raw_induct thy1 else (thy1 - |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])] + |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])] |> apfst hd |> Library.swap, @{thm TrueI}) and defs = big_rec_def :: part_rec_defs @@ -528,16 +528,16 @@ val (([bnd_mono', dom_subset', elim'], [defs', intrs']), thy3) = thy2 |> IndCases.declare big_rec_name make_cases - |> PureThy.add_thms + |> Global_Theory.add_thms [((Binding.name "bnd_mono", bnd_mono), []), ((Binding.name "dom_subset", dom_subset), []), ((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])] - ||>> (PureThy.add_thmss o map Thm.no_attributes) + ||>> (Global_Theory.add_thmss o map Thm.no_attributes) [(Binding.name "defs", defs), (Binding.name "intros", intrs)]; val (intrs'', thy4) = thy3 - |> PureThy.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs) + |> Global_Theory.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs) ||> Sign.parent_path; in (thy4, diff -r 32a00ff29d1a -r fe5722fce758 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/ZF/Tools/primrec_package.ML Mon Sep 20 16:05:25 2010 +0200 @@ -169,7 +169,7 @@ val ([def_thm], thy1) = thy |> Sign.add_path (Long_Name.base_name fname) - |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)]; + |> Global_Theory.add_defs false [Thm.no_attributes (apfst Binding.name def)]; val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info) val eqn_thms = @@ -179,10 +179,10 @@ val (eqn_thms', thy2) = thy1 - |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); + |> Global_Theory.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); val (_, thy3) = thy2 - |> PureThy.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])] + |> Global_Theory.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])] ||> Sign.parent_path; in (thy3, eqn_thms') end;