# HG changeset patch # User wenzelm # Date 1205968844 -3600 # Node ID 0dd2eab7b2969754e0296a635135207812ecd8f4 # Parent 0f65fa163304b694179e0d2178bb8a38208b3604 simplified get_thm(s): back to plain name argument; diff -r 0f65fa163304 -r 0dd2eab7b296 src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Wed Mar 19 22:50:42 2008 +0100 +++ b/src/FOL/ex/LocaleTest.thy Thu Mar 20 00:20:44 2008 +0100 @@ -19,7 +19,7 @@ ML {* fun check_thm name = let val thy = the_context (); - val thm = get_thm thy (Facts.Named (name, NONE)); + val thm = PureThy.get_thm thy name; val {prop, hyps, ...} = rep_thm thm; val prems = Logic.strip_imp_prems prop; val _ = if null hyps then () diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Import/proof_kernel.ML Thu Mar 20 00:20:44 2008 +0100 @@ -1277,10 +1277,10 @@ case get_hol4_mapping thyname thmname thy of SOME (SOME thmname) => let - val th1 = (SOME (PureThy.get_thm thy (Facts.Named (thmname, NONE))) + val th1 = (SOME (PureThy.get_thm thy thmname) handle ERROR _ => (case split_name thmname of - SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Facts.Named (listname, NONE)),idx-1)) + SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1)) handle _ => NONE) | NONE => NONE)) in @@ -2158,17 +2158,10 @@ add_dump ("syntax\n "^n^" :: _ "^syn) thy end -(*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table) -fun choose_upon_replay_history thy s dth = - case Symtab.lookup (!type_intro_replay_history) s of - NONE => (type_intro_replay_history := Symtab.update (s, ()) (!type_intro_replay_history); dth) - | SOME _ => HOLThm([], PureThy.get_thm thy (PureThy.Name s)) -*) - 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 (Facts.Named (thmname^"_@intern", NONE))) handle ERROR _ => hth) + HOLThm([], PureThy.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth) | _ => let val _ = message "TYPE_INTRO:" diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Matrix/cplex/matrixlp.ML --- a/src/HOL/Matrix/cplex/matrixlp.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Matrix/cplex/matrixlp.ML Thu Mar 20 00:20:44 2008 +0100 @@ -78,8 +78,8 @@ "SparseMatrix.sorted_sp_simps", "ComputeNumeral.number_norm", "ComputeNumeral.natnorm"] - fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} (Facts.Named (n, NONE))) - val ths = List.concat (map get_thms matrix_lemmas) + fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} n) + val ths = maps get_thms matrix_lemmas val computer = PCompute.make Compute.SML @{theory "Cplex"} ths [] in diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu Mar 20 00:20:44 2008 +0100 @@ -977,7 +977,7 @@ val s = post_last_dot(fst(qtn a)); fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t))))) = t | param_types _ = error "malformed induct-theorem in preprocess_td"; - val induct_rule = PureThy.get_thm sg (Facts.Named (s ^ ".induct", NONE)); + val induct_rule = PureThy.get_thm sg (s ^ ".induct"); val pl = param_types (concl_of induct_rule); val l = split_constrs sg (snd(qtn a)) pl (prems_of induct_rule); val ntl = new_types l; diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Thu Mar 20 00:20:44 2008 +0100 @@ -232,7 +232,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 (dynamic_thms thy5) + val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy5) ["at_def", ak_name ^ "_prm_" ^ ak_name ^ "_def", ak_name ^ "_prm_" ^ ak_name ^ ".simps", @@ -296,7 +296,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 (dynamic_thms thy7) + val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy7) ["pt_def", "pt_" ^ ak_name ^ "1", "pt_" ^ ak_name ^ "2", @@ -343,7 +343,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 (dynamic_thms thy11) + val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy11) ["fs_def", "fs_" ^ ak_name ^ "1"]; @@ -395,8 +395,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 (dynamic_thms thy') ["cp_def"]; - val cp1 = dynamic_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1"); + 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 name = "cp_"^ak_name^ "_"^ak_name'^"_inst"; val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type'); @@ -426,7 +426,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 (dynamic_thms thy') + val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy') ["disjoint_def", ak_name ^ "_prm_" ^ ak_name' ^ "_def", ak_name' ^ "_prm_" ^ ak_name ^ "_def"]; @@ -466,7 +466,7 @@ let val qu_name = Sign.full_name thy' ak_name'; val cls_name = Sign.full_name thy' ("pt_"^ak_name); - val at_inst = dynamic_thm thy' ("at_" ^ ak_name' ^ "_inst"); + val at_inst = PureThy.get_thm thy' ("at_" ^ ak_name' ^ "_inst"); val proof1 = EVERY [Class.intro_classes_tac [], rtac ((at_inst RS at_pt_inst) RS pt1) 1, @@ -474,7 +474,7 @@ rtac ((at_inst RS at_pt_inst) RS pt3) 1, atac 1]; val simp_s = HOL_basic_ss addsimps - maps (dynamic_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"]; + maps (PureThy.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"]; val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; in @@ -496,8 +496,8 @@ val thy18 = fold (fn ak_name => fn thy => let val cls_name = Sign.full_name thy ("pt_"^ak_name); - val at_thm = dynamic_thm thy ("at_"^ak_name^"_inst"); - val pt_inst = dynamic_thm thy ("pt_"^ak_name^"_inst"); + val at_thm = PureThy.get_thm thy ("at_"^ak_name^"_inst"); + val pt_inst = PureThy.get_thm thy ("pt_"^ak_name^"_inst"); fun pt_proof thm = EVERY [Class.intro_classes_tac [], @@ -546,11 +546,11 @@ val proof = (if ak_name = ak_name' then - let val at_thm = dynamic_thm thy' ("at_"^ak_name^"_inst"); + let val at_thm = PureThy.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 = dynamic_thm thy' ("dj_"^ak_name'^"_"^ak_name); + let val dj_inst = PureThy.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 @@ -568,7 +568,7 @@ val thy24 = fold (fn ak_name => fn thy => let val cls_name = Sign.full_name thy ("fs_"^ak_name); - val fs_inst = dynamic_thm thy ("fs_"^ak_name^"_inst"); + val fs_inst = PureThy.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; @@ -613,18 +613,18 @@ val proof = (if (ak_name'=ak_name'') then (let - val pt_inst = dynamic_thm thy'' ("pt_"^ak_name''^"_inst"); - val at_inst = dynamic_thm thy'' ("at_"^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"); in EVERY [Class.intro_classes_tac [], rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1] end) else (let - val dj_inst = dynamic_thm thy'' ("dj_"^ak_name''^"_"^ak_name'); + val dj_inst = PureThy.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name'); val simp_s = HOL_basic_ss addsimps ((dj_inst RS dj_pp_forget):: - (maps (dynamic_thms thy'') + (maps (PureThy.get_thms thy'') [ak_name' ^"_prm_"^ak_name^"_def", ak_name''^"_prm_"^ak_name^"_def"])); in @@ -647,9 +647,9 @@ fold (fn ak_name' => fn thy' => let val cls_name = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name'); - val cp_inst = dynamic_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst"); - val pt_inst = dynamic_thm thy' ("pt_"^ak_name^"_inst"); - val at_inst = dynamic_thm thy' ("at_"^ak_name^"_inst"); + 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"); fun cp_proof thm = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1]; @@ -804,27 +804,27 @@ (* list of all at_inst-theorems *) - val ats = map (fn ak => dynamic_thm thy32 ("at_"^ak^"_inst")) ak_names + val ats = map (fn ak => PureThy.get_thm thy32 ("at_"^ak^"_inst")) ak_names (* list of all pt_inst-theorems *) - val pts = map (fn ak => dynamic_thm thy32 ("pt_"^ak^"_inst")) ak_names + val pts = map (fn ak => PureThy.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 = dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst") + let fun cps_fun ak1 ak2 = PureThy.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 (dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")) + if ak1=ak2 then NONE else SOME (PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")) in map (fn aki => (List.mapPartial 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(dynamic_thm thy32 ("dj_"^ak2^"_"^ak1)) + if ak1=ak2 then NONE else SOME(PureThy.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 => dynamic_thm thy32 ("fs_"^ak^"_inst")) ak_names + val fss = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"_inst")) ak_names (* list of all at_inst-theorems *) - val fs_axs = map (fn ak => dynamic_thm thy32 ("fs_"^ak^"1")) ak_names + val fs_axs = map (fn ak => PureThy.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 0f65fa163304 -r 0dd2eab7b296 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Thu Mar 20 00:20:44 2008 +0100 @@ -57,7 +57,7 @@ res_inst_tac_term' tinst false (Tactic.make_elim_preserve th); fun get_dyn_thm thy name atom_name = - dynamic_thm thy name handle ERROR _ => + PureThy.get_thm thy name handle ERROR _ => raise ERROR ("The atom type "^atom_name^" is not defined."); (* End of function waiting to be in the library :o) *) @@ -146,8 +146,8 @@ val thy = theory_of_thm thm; val ctx = Context.init_proof thy; val ss = simpset_of thy; - val abs_fresh = dynamic_thms thy "abs_fresh"; - val fresh_perm_app = dynamic_thms thy "fresh_perm_app"; + val abs_fresh = PureThy.get_thms thy "abs_fresh"; + val fresh_perm_app = PureThy.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 (term_vars (prop_of exI))); diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Thu Mar 20 00:20:44 2008 +0100 @@ -273,19 +273,19 @@ (NominalPackage.fresh_const U T $ u $ t)) bvars) (ts ~~ binder_types (fastype_of p)))) prems; - val perm_pi_simp = dynamic_thms thy "perm_pi_simp"; - val pt2_atoms = map (fn aT => dynamic_thm thy + val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; + val pt2_atoms = map (fn aT => PureThy.get_thm thy ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2")) atomTs; val eqvt_ss = HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc ["Fun.id"]]; - val fresh_bij = dynamic_thms thy "fresh_bij"; - val perm_bij = dynamic_thms thy "perm_bij"; - val fs_atoms = map (fn aT => dynamic_thm thy + 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 ("fs_" ^ Sign.base_name (fst (dest_Type aT)) ^ "1")) atomTs; - val exists_fresh' = dynamic_thms thy "exists_fresh'"; - val fresh_atm = dynamic_thms thy "fresh_atm"; - val calc_atm = dynamic_thms thy "calc_atm"; - val perm_fresh_fresh = dynamic_thms thy "perm_fresh_fresh"; + val exists_fresh' = PureThy.get_thms thy "exists_fresh'"; + val fresh_atm = PureThy.get_thms thy "fresh_atm"; + val calc_atm = PureThy.get_thms thy "calc_atm"; + val perm_fresh_fresh = PureThy.get_thms thy "perm_fresh_fresh"; fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) = let @@ -604,7 +604,7 @@ | xs => error ("No such atoms: " ^ commas xs); atoms) end; - val perm_pi_simp = dynamic_thms thy "perm_pi_simp"; + val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; val eqvt_ss = HOL_basic_ss addsimps (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs [mk_perm_bool_simproc names]; diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Thu Mar 20 00:20:44 2008 +0100 @@ -140,8 +140,8 @@ let val a' = Sign.base_name a; val b' = Sign.base_name b; - val cp = dynamic_thm thy ("cp_" ^ a' ^ "_" ^ b' ^ "_inst"); - val dj = dynamic_thm thy ("dj_" ^ b' ^ "_" ^ a'); + val cp = PureThy.get_thm thy ("cp_" ^ a' ^ "_" ^ b' ^ "_inst"); + val dj = PureThy.get_thm thy ("dj_" ^ b' ^ "_" ^ a'); val dj_cp' = [cp, dj] MRS dj_cp; val cert = SOME o cterm_of thy in @@ -309,7 +309,7 @@ val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names)); val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types); - val perm_fun_def = dynamic_thm thy2 "perm_fun_def"; + val perm_fun_def = PureThy.get_thm thy2 "perm_fun_def"; val unfolded_perm_eq_thms = if length descr = length new_type_names then [] @@ -353,17 +353,17 @@ val _ = warning "perm_append_thms"; (*FIXME: these should be looked up statically*) - val at_pt_inst = dynamic_thm thy2 "at_pt_inst"; - val pt2 = dynamic_thm thy2 "pt2"; + val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst"; + val pt2 = PureThy.get_thm thy2 "pt2"; val perm_append_thms = List.concat (map (fn a => let val permT = mk_permT (Type (a, [])); val pi1 = Free ("pi1", permT); val pi2 = Free ("pi2", permT); - val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst"); + val pt_inst = PureThy.get_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst"); val pt2' = pt_inst RS pt2; - val pt2_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a); + val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a); in List.take (map standard (split_conj_thm (Goal.prove_global thy2 [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj @@ -385,8 +385,8 @@ val _ = warning "perm_eq_thms"; - val pt3 = dynamic_thm thy2 "pt3"; - val pt3_rev = dynamic_thm thy2 "pt3_rev"; + val pt3 = PureThy.get_thm thy2 "pt3"; + val pt3_rev = PureThy.get_thm thy2 "pt3_rev"; val perm_eq_thms = List.concat (map (fn a => let @@ -394,11 +394,11 @@ val pi1 = Free ("pi1", permT); val pi2 = Free ("pi2", permT); (*FIXME: not robust - better access these theorems using NominalData?*) - val at_inst = dynamic_thm thy2 ("at_" ^ Sign.base_name a ^ "_inst"); - val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst"); + val at_inst = PureThy.get_thm thy2 ("at_" ^ Sign.base_name a ^ "_inst"); + val pt_inst = PureThy.get_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst"); val pt3' = pt_inst RS pt3; val pt3_rev' = at_inst RS (pt_inst RS pt3_rev); - val pt3_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a); + val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a); in List.take (map standard (split_conj_thm (Goal.prove_global thy2 [] [] (Logic.mk_implies (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq", @@ -419,11 +419,11 @@ (**** prove pi1 \ (pi2 \ t) = (pi1 \ pi2) \ (pi1 \ t) ****) - val cp1 = dynamic_thm thy2 "cp1"; - val dj_cp = dynamic_thm thy2 "dj_cp"; - val pt_perm_compose = dynamic_thm thy2 "pt_perm_compose"; - val pt_perm_compose_rev = dynamic_thm thy2 "pt_perm_compose_rev"; - val dj_perm_perm_forget = dynamic_thm thy2 "dj_perm_perm_forget"; + 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"; fun composition_instance name1 name2 thy = let @@ -435,15 +435,15 @@ val augment = map_type_tfree (fn (x, S) => TFree (x, cp_class :: S)); val Ts = map (augment o body_type) perm_types; - val cp_inst = dynamic_thm thy ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst"); + val cp_inst = PureThy.get_thm thy ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst"); val simps = simpset_of thy addsimps (perm_fun_def :: (if name1 <> name2 then - let val dj = dynamic_thm thy ("dj_" ^ name2' ^ "_" ^ name1') + let val dj = PureThy.get_thm thy ("dj_" ^ name2' ^ "_" ^ name1') in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end else let - val at_inst = dynamic_thm thy ("at_" ^ name1' ^ "_inst"); - val pt_inst = dynamic_thm thy ("pt_" ^ name1' ^ "_inst"); + val at_inst = PureThy.get_thm thy ("at_" ^ name1' ^ "_inst"); + val pt_inst = PureThy.get_thm thy ("pt_" ^ name1' ^ "_inst"); in [cp_inst RS cp1 RS sym, at_inst RS (pt_inst RS pt_perm_compose) RS sym, @@ -571,7 +571,7 @@ val _ = warning "proving closure under permutation..."; - val abs_perm = dynamic_thms thy4 "abs_perm"; + val abs_perm = PureThy.get_thms thy4 "abs_perm"; val perm_indnames' = List.mapPartial (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x) @@ -656,7 +656,7 @@ asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1, asm_full_simp_tac (simpset_of thy addsimps [Rep RS perm_closed RS Abs_inverse]) 1, - asm_full_simp_tac (HOL_basic_ss addsimps [dynamic_thm thy + asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy ("pt_" ^ Sign.base_name atom ^ "3")]) 1]) thy) (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms); @@ -670,7 +670,7 @@ let val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2; val class = Sign.intern_class thy name; - val cp1' = dynamic_thm thy (name ^ "_inst") RS cp1 + val cp1' = PureThy.get_thm thy (name ^ "_inst") RS cp1 in fold (fn ((((((Abs_inverse, Rep), perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy => AxClass.prove_arity @@ -920,8 +920,8 @@ (** prove injectivity of constructors **) val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms; - val alpha = dynamic_thms thy8 "alpha"; - val abs_fresh = dynamic_thms thy8 "abs_fresh"; + val alpha = PureThy.get_thms thy8 "alpha"; + val abs_fresh = PureThy.get_thms thy8 "abs_fresh"; val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) => let val T = nth_dtyp' i @@ -1066,8 +1066,8 @@ val indnames = DatatypeProp.make_tnames recTs; - val abs_supp = dynamic_thms thy8 "abs_supp"; - val supp_atm = dynamic_thms thy8 "supp_atm"; + val abs_supp = PureThy.get_thms thy8 "abs_supp"; + val supp_atm = PureThy.get_thms thy8 "supp_atm"; val finite_supp_thms = map (fn atom => let val atomT = Type (atom, []) @@ -1080,7 +1080,7 @@ (fn _ => indtac dt_induct indnames 1 THEN ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps (abs_supp @ supp_atm @ - dynamic_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @ + PureThy.get_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @ List.concat supp_thms))))), length new_type_names)) end) atoms; @@ -1207,23 +1207,23 @@ (descr'' ~~ recTs ~~ tnames))); val fin_set_supp = map (fn Type (s, _) => - dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS + PureThy.get_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS at_fin_set_supp) dt_atomTs; val fin_set_fresh = map (fn Type (s, _) => - dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS + PureThy.get_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS at_fin_set_fresh) dt_atomTs; val pt1_atoms = map (fn Type (s, _) => - dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs; + PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs; val pt2_atoms = map (fn Type (s, _) => - dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs; - val exists_fresh' = dynamic_thms thy9 "exists_fresh'"; - val fs_atoms = dynamic_thms thy9 "fin_supp"; - val abs_supp = dynamic_thms thy9 "abs_supp"; - val perm_fresh_fresh = dynamic_thms thy9 "perm_fresh_fresh"; - val calc_atm = dynamic_thms thy9 "calc_atm"; - val fresh_atm = dynamic_thms thy9 "fresh_atm"; - val fresh_left = dynamic_thms thy9 "fresh_left"; - val perm_swap = dynamic_thms thy9 "perm_swap"; + PureThy.get_thm thy9 ("pt_" ^ Sign.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"; fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) = let @@ -1496,8 +1496,8 @@ (** equivariance **) - val fresh_bij = dynamic_thms thy11 "fresh_bij"; - val perm_bij = dynamic_thms thy11 "perm_bij"; + val fresh_bij = PureThy.get_thms thy11 "fresh_bij"; + val perm_bij = PureThy.get_thms thy11 "perm_bij"; val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT => let @@ -1535,7 +1535,7 @@ val rec_fin_supp_thms = map (fn aT => let val name = Sign.base_name (fst (dest_Type aT)); - val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1"); + val fs_name = PureThy.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 @@ -1568,7 +1568,7 @@ val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) => let val name = Sign.base_name (fst (dest_Type aT)); - val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1"); + val fs_name = PureThy.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) diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Nominal/nominal_permeq.ML Thu Mar 20 00:20:44 2008 +0100 @@ -71,8 +71,8 @@ val supports_fresh_rule = @{thm "supports_fresh"}; (* pulls out dynamically a thm via the proof state *) -fun global_thms st name = PureThy.get_thms (theory_of_thm st) (Facts.Named (name, NONE)); -fun global_thm st name = PureThy.get_thm (theory_of_thm st) (Facts.Named (name, NONE)); +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; (* needed in the process of fully simplifying permutations *) @@ -111,8 +111,8 @@ (if (applicable_app f) then let val name = Sign.base_name n - val at_inst = dynamic_thm sg ("at_" ^ name ^ "_inst") - val pt_inst = dynamic_thm sg ("pt_" ^ name ^ "_inst") + val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst") + val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst") in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end else NONE) | _ => NONE @@ -146,7 +146,7 @@ ("general simplification of permutations", fn st => let val ss' = Simplifier.theory_context (theory_of_thm st) ss - addsimps ((List.concat (map (global_thms st) dyn_thms))@eqvt_thms) + addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms) delcongs weak_congs addcongs strong_congs addsimprocs [perm_simproc_fun, perm_simproc_app] @@ -198,13 +198,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 ([dynamic_thm sg ("pt_"^tname'^"_inst"), - dynamic_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux))) + (mk_meta_eq ([PureThy.get_thm sg ("pt_"^tname'^"_inst"), + PureThy.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 (dynamic_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS + (mk_meta_eq (PureThy.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS cp1_aux))) else NONE end @@ -307,7 +307,7 @@ Logic.strip_assums_concl (hd (prems_of supports_rule')); val supports_rule'' = Drule.cterm_instantiate [(cert (head_of S), cert s')] supports_rule' - val fin_supp = global_thms st ("fin_supp") + val fin_supp = dynamic_thms st ("fin_supp") val ss' = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp in (tactical ("guessing of the right supports-set", @@ -326,8 +326,8 @@ fun fresh_guess_tac tactical ss i st = let val goal = List.nth(cprems_of st, i-1) - val fin_supp = global_thms st ("fin_supp") - val fresh_atm = global_thms st ("fresh_atm") + val fin_supp = dynamic_thms st ("fin_supp") + val fresh_atm = dynamic_thms st ("fresh_atm") val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp in diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Mar 20 00:20:44 2008 +0100 @@ -10,9 +10,6 @@ respectively the lemma from the data-slot. *) -fun dynamic_thm thy name = PureThy.get_thm thy (Facts.Named (name, NONE)); -fun dynamic_thms thy name = PureThy.get_thms thy (Facts.Named (name, NONE)); - signature NOMINAL_THMDECLS = sig val print_data: Proof.context -> unit @@ -83,7 +80,7 @@ let val mypi = Thm.cterm_of ctx (Var (pi,typi)) val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi)) - val perm_pi_simp = dynamic_thms ctx "perm_pi_simp" + val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp" in EVERY [tactic ("iffI applied",rtac iffI 1), tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)), diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Thu Mar 20 00:20:44 2008 +0100 @@ -339,7 +339,7 @@ fun neq_x_y ctxt x y name = (let - val dist_thm = the (try (ProofContext.get_thm ctxt) (Facts.Named (name, NONE))); + val dist_thm = the (try (ProofContext.get_thm ctxt) name); val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; val tree = term_of ctree; val x_path = the (find_tree x tree); diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Statespace/state_space.ML Thu Mar 20 00:20:44 2008 +0100 @@ -270,7 +270,7 @@ fun solve_tac ctxt (_,i) st = let - val distinct_thm = ProofContext.get_thm ctxt (Facts.Named (dist_thm_name, NONE)); + val distinct_thm = ProofContext.get_thm ctxt dist_thm_name; val goal = List.nth (cprems_of st,i-1); val rule = DistinctTreeProver.distinct_implProver distinct_thm goal; in EVERY [rtac rule i] st diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Tools/datatype_package.ML Thu Mar 20 00:20:44 2008 +0100 @@ -391,7 +391,7 @@ | ManyConstrs (thm, simpset) => let val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] = - map (fn a => get_thm (ThyInfo.the_theory "Datatype" thy) (Facts.Named (a, NONE))) + map (PureThy.get_thm (ThyInfo.the_theory "Datatype" thy)) ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]; in Goal.prove (Simplifier.the_context ss) [] [] eq_t (K diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Mar 20 00:20:44 2008 +0100 @@ -57,11 +57,10 @@ val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq, In0_not_In1, In1_not_In0, - Lim_inject, Suml_inject, Sumr_inject] = - map (fn a => get_thm Datatype_thy (Facts.Named (a, NONE))) - ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", - "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", - "Lim_inject", "Suml_inject", "Sumr_inject"]; + Lim_inject, Suml_inject, Sumr_inject] = map (PureThy.get_thm Datatype_thy) + ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", + "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", + "Lim_inject", "Suml_inject", "Sumr_inject"]; val descr' = List.concat descr; diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Thu Mar 20 00:20:44 2008 +0100 @@ -276,7 +276,7 @@ fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) = let val qualifier = NameSpace.qualifier (name_of_thm induct); - val inducts = PureThy.get_thms thy (Facts.Named (NameSpace.qualified qualifier "inducts", NONE)); + val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts"); val iTs = term_tvars (prop_of (hd intrs)); val ar = length vs + length iTs; val params = InductivePackage.params_of raw_induct; diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOLCF/IOA/meta_theory/ioa_package.ML --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Thu Mar 20 00:20:44 2008 +0100 @@ -98,7 +98,7 @@ fun unqualify s = implode(rev(afpl(rev(explode s)))); val q_atypstr = act_name thy atyp; val uq_atypstr = unqualify q_atypstr; -val prem = prems_of (PureThy.get_thm thy (Facts.Named (uq_atypstr ^ ".induct", NONE))); +val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct")); in extract_constrs thy prem handle malformed => @@ -284,7 +284,7 @@ let fun left_of (( _ $ left) $ _) = left | left_of _ = raise malformed; -val aut_def = concl_of (PureThy.get_thm thy (Facts.Named (aut_name ^ "_def", NONE))); +val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def")); in (#T(rep_cterm(cterm_of thy (left_of aut_def)))) handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Thu Mar 20 00:20:44 2008 +0100 @@ -126,7 +126,7 @@ (* ----- getting the axioms and definitions --------------------------------- *) local - fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE)); + fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); in val ax_abs_iso = ga "abs_iso" dname; val ax_rep_iso = ga "rep_iso" dname; @@ -612,7 +612,7 @@ (* ----- getting the composite axiom and definitions ------------------------ *) local - fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE)); + fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); in val axs_reach = map (ga "reach" ) dnames; val axs_take_def = map (ga "take_def" ) dnames; @@ -622,8 +622,8 @@ end; local - fun gt s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE)); - fun gts s dn = PureThy.get_thms thy (Facts.Named (dn ^ "." ^ s, NONE)); + fun gt s dn = PureThy.get_thm thy (dn ^ "." ^ s); + fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s); in val cases = map (gt "casedist" ) dnames; val con_rews = maps (gts "con_rews" ) dnames; diff -r 0f65fa163304 -r 0dd2eab7b296 src/HOLCF/Tools/fixrec_package.ML --- a/src/HOLCF/Tools/fixrec_package.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/HOLCF/Tools/fixrec_package.ML Thu Mar 20 00:20:44 2008 +0100 @@ -267,7 +267,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 (Facts.Named (cname^"_unfold", NONE)); + val unfold_thm = PureThy.get_thm thy (cname^"_unfold"); val simp = Goal.prove_global thy [] [] eq (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]); in simp end; diff -r 0f65fa163304 -r 0dd2eab7b296 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/Pure/Proof/extraction.ML Thu Mar 20 00:20:44 2008 +0100 @@ -765,8 +765,7 @@ K.thy_decl (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >> (fn xs => Toplevel.theory (fn thy => add_realizers - (map (fn (((a, vs), s1), s2) => - (PureThy.get_thm thy (Facts.Named (a, NONE)), (vs, s1, s2))) xs) thy))); + (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy))); val _ = OuterSyntax.command "realizability" @@ -781,7 +780,7 @@ val _ = OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy => - extract (map (fn (a, vs) => (PureThy.get_thm thy (Facts.Named (a, NONE)), vs)) xs) thy))); + extract (map (apfst (PureThy.get_thm thy)) xs) thy))); val etype_of = etype_of o add_syntax; diff -r 0f65fa163304 -r 0dd2eab7b296 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 20 00:20:44 2008 +0100 @@ -712,7 +712,7 @@ What we want is mapping onto simple PGIP name/context model. *) val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *) val thy = Context.theory_of_proof ctx - val ths = [PureThy.get_thm thy (Facts.Named (thmname, NONE))] + val ths = [PureThy.get_thm thy thmname] val deps = filter_out (equal "") (Symtab.keys (fold Proofterm.thms_of_proof (map Thm.proof_of ths) Symtab.empty)) @@ -764,7 +764,7 @@ [] (* asms *) th)) - fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Facts.Named (name, NONE))) + fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name) val string_of_thy = Output.output o Pretty.string_of o (ProofDisplay.pretty_full_theory false) diff -r 0f65fa163304 -r 0dd2eab7b296 src/Tools/Compute_Oracle/linker.ML --- a/src/Tools/Compute_Oracle/linker.ML Wed Mar 19 22:50:42 2008 +0100 +++ b/src/Tools/Compute_Oracle/linker.ML Thu Mar 20 00:20:44 2008 +0100 @@ -192,7 +192,7 @@ fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs local - fun get_thm thmname = PureThy.get_thm (theory "Main") (Facts.Named (thmname, NONE)) + fun get_thm thmname = PureThy.get_thm (theory "Main") thmname val eq_th = get_thm "HOL.eq_reflection" in fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)