--- 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 ()
--- 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:"
--- 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
--- 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;
--- 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;
--- 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)));
--- 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];
--- 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 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> 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)
--- 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
--- 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)),
--- 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);
--- 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
--- 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
--- 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;
--- 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;
--- 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")
--- 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;
--- 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;
--- 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;
--- 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)
--- 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)