1.1 --- a/src/FOL/ex/LocaleTest.thy Wed Mar 19 22:50:42 2008 +0100
1.2 +++ b/src/FOL/ex/LocaleTest.thy Thu Mar 20 00:20:44 2008 +0100
1.3 @@ -19,7 +19,7 @@
1.4 ML {*
1.5 fun check_thm name = let
1.6 val thy = the_context ();
1.7 - val thm = get_thm thy (Facts.Named (name, NONE));
1.8 + val thm = PureThy.get_thm thy name;
1.9 val {prop, hyps, ...} = rep_thm thm;
1.10 val prems = Logic.strip_imp_prems prop;
1.11 val _ = if null hyps then ()
2.1 --- a/src/HOL/Import/proof_kernel.ML Wed Mar 19 22:50:42 2008 +0100
2.2 +++ b/src/HOL/Import/proof_kernel.ML Thu Mar 20 00:20:44 2008 +0100
2.3 @@ -1277,10 +1277,10 @@
2.4 case get_hol4_mapping thyname thmname thy of
2.5 SOME (SOME thmname) =>
2.6 let
2.7 - val th1 = (SOME (PureThy.get_thm thy (Facts.Named (thmname, NONE)))
2.8 + val th1 = (SOME (PureThy.get_thm thy thmname)
2.9 handle ERROR _ =>
2.10 (case split_name thmname of
2.11 - SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Facts.Named (listname, NONE)),idx-1))
2.12 + SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
2.13 handle _ => NONE)
2.14 | NONE => NONE))
2.15 in
2.16 @@ -2158,17 +2158,10 @@
2.17 add_dump ("syntax\n "^n^" :: _ "^syn) thy
2.18 end
2.19
2.20 -(*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table)
2.21 -fun choose_upon_replay_history thy s dth =
2.22 - case Symtab.lookup (!type_intro_replay_history) s of
2.23 - NONE => (type_intro_replay_history := Symtab.update (s, ()) (!type_intro_replay_history); dth)
2.24 - | SOME _ => HOLThm([], PureThy.get_thm thy (PureThy.Name s))
2.25 -*)
2.26 -
2.27 fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
2.28 case HOL4DefThy.get thy of
2.29 Replaying _ => (thy,
2.30 - HOLThm([], PureThy.get_thm thy (Facts.Named (thmname^"_@intern", NONE))) handle ERROR _ => hth)
2.31 + HOLThm([], PureThy.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
2.32 | _ =>
2.33 let
2.34 val _ = message "TYPE_INTRO:"
3.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML Wed Mar 19 22:50:42 2008 +0100
3.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML Thu Mar 20 00:20:44 2008 +0100
3.3 @@ -78,8 +78,8 @@
3.4 "SparseMatrix.sorted_sp_simps",
3.5 "ComputeNumeral.number_norm",
3.6 "ComputeNumeral.natnorm"]
3.7 - fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} (Facts.Named (n, NONE)))
3.8 - val ths = List.concat (map get_thms matrix_lemmas)
3.9 + fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} n)
3.10 + val ths = maps get_thms matrix_lemmas
3.11 val computer = PCompute.make Compute.SML @{theory "Cplex"} ths []
3.12 in
3.13
4.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML Wed Mar 19 22:50:42 2008 +0100
4.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu Mar 20 00:20:44 2008 +0100
4.3 @@ -977,7 +977,7 @@
4.4 val s = post_last_dot(fst(qtn a));
4.5 fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t))))) = t |
4.6 param_types _ = error "malformed induct-theorem in preprocess_td";
4.7 - val induct_rule = PureThy.get_thm sg (Facts.Named (s ^ ".induct", NONE));
4.8 + val induct_rule = PureThy.get_thm sg (s ^ ".induct");
4.9 val pl = param_types (concl_of induct_rule);
4.10 val l = split_constrs sg (snd(qtn a)) pl (prems_of induct_rule);
4.11 val ntl = new_types l;
5.1 --- a/src/HOL/Nominal/nominal_atoms.ML Wed Mar 19 22:50:42 2008 +0100
5.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Thu Mar 20 00:20:44 2008 +0100
5.3 @@ -232,7 +232,7 @@
5.4 val i_type = Type(ak_name_qu,[]);
5.5 val cat = Const ("Nominal.at",(Term.itselfT i_type) --> HOLogic.boolT);
5.6 val at_type = Logic.mk_type i_type;
5.7 - val simp_s = HOL_ss addsimps maps (dynamic_thms thy5)
5.8 + val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy5)
5.9 ["at_def",
5.10 ak_name ^ "_prm_" ^ ak_name ^ "_def",
5.11 ak_name ^ "_prm_" ^ ak_name ^ ".simps",
5.12 @@ -296,7 +296,7 @@
5.13 val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
5.14 val pt_type = Logic.mk_type i_type1;
5.15 val at_type = Logic.mk_type i_type2;
5.16 - val simp_s = HOL_ss addsimps maps (dynamic_thms thy7)
5.17 + val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy7)
5.18 ["pt_def",
5.19 "pt_" ^ ak_name ^ "1",
5.20 "pt_" ^ ak_name ^ "2",
5.21 @@ -343,7 +343,7 @@
5.22 (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
5.23 val fs_type = Logic.mk_type i_type1;
5.24 val at_type = Logic.mk_type i_type2;
5.25 - val simp_s = HOL_ss addsimps maps (dynamic_thms thy11)
5.26 + val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy11)
5.27 ["fs_def",
5.28 "fs_" ^ ak_name ^ "1"];
5.29
5.30 @@ -395,8 +395,8 @@
5.31 val at_type = Logic.mk_type i_type1;
5.32 val at_type' = Logic.mk_type i_type2;
5.33 val cp_type = Logic.mk_type i_type0;
5.34 - val simp_s = HOL_basic_ss addsimps maps (dynamic_thms thy') ["cp_def"];
5.35 - val cp1 = dynamic_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1");
5.36 + val simp_s = HOL_basic_ss addsimps maps (PureThy.get_thms thy') ["cp_def"];
5.37 + val cp1 = PureThy.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1");
5.38
5.39 val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
5.40 val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
5.41 @@ -426,7 +426,7 @@
5.42 (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
5.43 val at_type = Logic.mk_type i_type1;
5.44 val at_type' = Logic.mk_type i_type2;
5.45 - val simp_s = HOL_ss addsimps maps (dynamic_thms thy')
5.46 + val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy')
5.47 ["disjoint_def",
5.48 ak_name ^ "_prm_" ^ ak_name' ^ "_def",
5.49 ak_name' ^ "_prm_" ^ ak_name ^ "_def"];
5.50 @@ -466,7 +466,7 @@
5.51 let
5.52 val qu_name = Sign.full_name thy' ak_name';
5.53 val cls_name = Sign.full_name thy' ("pt_"^ak_name);
5.54 - val at_inst = dynamic_thm thy' ("at_" ^ ak_name' ^ "_inst");
5.55 + val at_inst = PureThy.get_thm thy' ("at_" ^ ak_name' ^ "_inst");
5.56
5.57 val proof1 = EVERY [Class.intro_classes_tac [],
5.58 rtac ((at_inst RS at_pt_inst) RS pt1) 1,
5.59 @@ -474,7 +474,7 @@
5.60 rtac ((at_inst RS at_pt_inst) RS pt3) 1,
5.61 atac 1];
5.62 val simp_s = HOL_basic_ss addsimps
5.63 - maps (dynamic_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"];
5.64 + maps (PureThy.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"];
5.65 val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
5.66
5.67 in
5.68 @@ -496,8 +496,8 @@
5.69 val thy18 = fold (fn ak_name => fn thy =>
5.70 let
5.71 val cls_name = Sign.full_name thy ("pt_"^ak_name);
5.72 - val at_thm = dynamic_thm thy ("at_"^ak_name^"_inst");
5.73 - val pt_inst = dynamic_thm thy ("pt_"^ak_name^"_inst");
5.74 + val at_thm = PureThy.get_thm thy ("at_"^ak_name^"_inst");
5.75 + val pt_inst = PureThy.get_thm thy ("pt_"^ak_name^"_inst");
5.76
5.77 fun pt_proof thm =
5.78 EVERY [Class.intro_classes_tac [],
5.79 @@ -546,11 +546,11 @@
5.80 val proof =
5.81 (if ak_name = ak_name'
5.82 then
5.83 - let val at_thm = dynamic_thm thy' ("at_"^ak_name^"_inst");
5.84 + let val at_thm = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
5.85 in EVERY [Class.intro_classes_tac [],
5.86 rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
5.87 else
5.88 - let val dj_inst = dynamic_thm thy' ("dj_"^ak_name'^"_"^ak_name);
5.89 + let val dj_inst = PureThy.get_thm thy' ("dj_"^ak_name'^"_"^ak_name);
5.90 val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
5.91 in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end)
5.92 in
5.93 @@ -568,7 +568,7 @@
5.94 val thy24 = fold (fn ak_name => fn thy =>
5.95 let
5.96 val cls_name = Sign.full_name thy ("fs_"^ak_name);
5.97 - val fs_inst = dynamic_thm thy ("fs_"^ak_name^"_inst");
5.98 + val fs_inst = PureThy.get_thm thy ("fs_"^ak_name^"_inst");
5.99 fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1];
5.100
5.101 val fs_thm_unit = fs_unit_inst;
5.102 @@ -613,18 +613,18 @@
5.103 val proof =
5.104 (if (ak_name'=ak_name'') then
5.105 (let
5.106 - val pt_inst = dynamic_thm thy'' ("pt_"^ak_name''^"_inst");
5.107 - val at_inst = dynamic_thm thy'' ("at_"^ak_name''^"_inst");
5.108 + val pt_inst = PureThy.get_thm thy'' ("pt_"^ak_name''^"_inst");
5.109 + val at_inst = PureThy.get_thm thy'' ("at_"^ak_name''^"_inst");
5.110 in
5.111 EVERY [Class.intro_classes_tac [],
5.112 rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
5.113 end)
5.114 else
5.115 (let
5.116 - val dj_inst = dynamic_thm thy'' ("dj_"^ak_name''^"_"^ak_name');
5.117 + val dj_inst = PureThy.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name');
5.118 val simp_s = HOL_basic_ss addsimps
5.119 ((dj_inst RS dj_pp_forget)::
5.120 - (maps (dynamic_thms thy'')
5.121 + (maps (PureThy.get_thms thy'')
5.122 [ak_name' ^"_prm_"^ak_name^"_def",
5.123 ak_name''^"_prm_"^ak_name^"_def"]));
5.124 in
5.125 @@ -647,9 +647,9 @@
5.126 fold (fn ak_name' => fn thy' =>
5.127 let
5.128 val cls_name = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
5.129 - val cp_inst = dynamic_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
5.130 - val pt_inst = dynamic_thm thy' ("pt_"^ak_name^"_inst");
5.131 - val at_inst = dynamic_thm thy' ("at_"^ak_name^"_inst");
5.132 + val cp_inst = PureThy.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
5.133 + val pt_inst = PureThy.get_thm thy' ("pt_"^ak_name^"_inst");
5.134 + val at_inst = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
5.135
5.136 fun cp_proof thm = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1];
5.137
5.138 @@ -804,27 +804,27 @@
5.139
5.140
5.141 (* list of all at_inst-theorems *)
5.142 - val ats = map (fn ak => dynamic_thm thy32 ("at_"^ak^"_inst")) ak_names
5.143 + val ats = map (fn ak => PureThy.get_thm thy32 ("at_"^ak^"_inst")) ak_names
5.144 (* list of all pt_inst-theorems *)
5.145 - val pts = map (fn ak => dynamic_thm thy32 ("pt_"^ak^"_inst")) ak_names
5.146 + val pts = map (fn ak => PureThy.get_thm thy32 ("pt_"^ak^"_inst")) ak_names
5.147 (* list of all cp_inst-theorems as a collection of lists*)
5.148 val cps =
5.149 - let fun cps_fun ak1 ak2 = dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")
5.150 + let fun cps_fun ak1 ak2 = PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")
5.151 in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end;
5.152 (* list of all cp_inst-theorems that have different atom types *)
5.153 val cps' =
5.154 let fun cps'_fun ak1 ak2 =
5.155 - if ak1=ak2 then NONE else SOME (dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
5.156 + if ak1=ak2 then NONE else SOME (PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
5.157 in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end;
5.158 (* list of all dj_inst-theorems *)
5.159 val djs =
5.160 let fun djs_fun ak1 ak2 =
5.161 - if ak1=ak2 then NONE else SOME(dynamic_thm thy32 ("dj_"^ak2^"_"^ak1))
5.162 + if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 ("dj_"^ak2^"_"^ak1))
5.163 in map_filter I (map_product djs_fun ak_names ak_names) end;
5.164 (* list of all fs_inst-theorems *)
5.165 - val fss = map (fn ak => dynamic_thm thy32 ("fs_"^ak^"_inst")) ak_names
5.166 + val fss = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"_inst")) ak_names
5.167 (* list of all at_inst-theorems *)
5.168 - val fs_axs = map (fn ak => dynamic_thm thy32 ("fs_"^ak^"1")) ak_names
5.169 + val fs_axs = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"1")) ak_names
5.170
5.171 fun inst_pt thms = maps (fn ti => instR ti pts) thms;
5.172 fun inst_at thms = maps (fn ti => instR ti ats) thms;
6.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Mar 19 22:50:42 2008 +0100
6.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Thu Mar 20 00:20:44 2008 +0100
6.3 @@ -57,7 +57,7 @@
6.4 res_inst_tac_term' tinst false (Tactic.make_elim_preserve th);
6.5
6.6 fun get_dyn_thm thy name atom_name =
6.7 - dynamic_thm thy name handle ERROR _ =>
6.8 + PureThy.get_thm thy name handle ERROR _ =>
6.9 raise ERROR ("The atom type "^atom_name^" is not defined.");
6.10
6.11 (* End of function waiting to be in the library :o) *)
6.12 @@ -146,8 +146,8 @@
6.13 val thy = theory_of_thm thm;
6.14 val ctx = Context.init_proof thy;
6.15 val ss = simpset_of thy;
6.16 - val abs_fresh = dynamic_thms thy "abs_fresh";
6.17 - val fresh_perm_app = dynamic_thms thy "fresh_perm_app";
6.18 + val abs_fresh = PureThy.get_thms thy "abs_fresh";
6.19 + val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
6.20 val ss' = ss addsimps fresh_prod::abs_fresh;
6.21 val ss'' = ss' addsimps fresh_perm_app;
6.22 val x = hd (tl (term_vars (prop_of exI)));
7.1 --- a/src/HOL/Nominal/nominal_inductive.ML Wed Mar 19 22:50:42 2008 +0100
7.2 +++ b/src/HOL/Nominal/nominal_inductive.ML Thu Mar 20 00:20:44 2008 +0100
7.3 @@ -273,19 +273,19 @@
7.4 (NominalPackage.fresh_const U T $ u $ t)) bvars)
7.5 (ts ~~ binder_types (fastype_of p)))) prems;
7.6
7.7 - val perm_pi_simp = dynamic_thms thy "perm_pi_simp";
7.8 - val pt2_atoms = map (fn aT => dynamic_thm thy
7.9 + val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
7.10 + val pt2_atoms = map (fn aT => PureThy.get_thm thy
7.11 ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
7.12 val eqvt_ss = HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
7.13 addsimprocs [mk_perm_bool_simproc ["Fun.id"]];
7.14 - val fresh_bij = dynamic_thms thy "fresh_bij";
7.15 - val perm_bij = dynamic_thms thy "perm_bij";
7.16 - val fs_atoms = map (fn aT => dynamic_thm thy
7.17 + val fresh_bij = PureThy.get_thms thy "fresh_bij";
7.18 + val perm_bij = PureThy.get_thms thy "perm_bij";
7.19 + val fs_atoms = map (fn aT => PureThy.get_thm thy
7.20 ("fs_" ^ Sign.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
7.21 - val exists_fresh' = dynamic_thms thy "exists_fresh'";
7.22 - val fresh_atm = dynamic_thms thy "fresh_atm";
7.23 - val calc_atm = dynamic_thms thy "calc_atm";
7.24 - val perm_fresh_fresh = dynamic_thms thy "perm_fresh_fresh";
7.25 + val exists_fresh' = PureThy.get_thms thy "exists_fresh'";
7.26 + val fresh_atm = PureThy.get_thms thy "fresh_atm";
7.27 + val calc_atm = PureThy.get_thms thy "calc_atm";
7.28 + val perm_fresh_fresh = PureThy.get_thms thy "perm_fresh_fresh";
7.29
7.30 fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) =
7.31 let
7.32 @@ -604,7 +604,7 @@
7.33 | xs => error ("No such atoms: " ^ commas xs);
7.34 atoms)
7.35 end;
7.36 - val perm_pi_simp = dynamic_thms thy "perm_pi_simp";
7.37 + val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
7.38 val eqvt_ss = HOL_basic_ss addsimps
7.39 (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
7.40 [mk_perm_bool_simproc names];
8.1 --- a/src/HOL/Nominal/nominal_package.ML Wed Mar 19 22:50:42 2008 +0100
8.2 +++ b/src/HOL/Nominal/nominal_package.ML Thu Mar 20 00:20:44 2008 +0100
8.3 @@ -140,8 +140,8 @@
8.4 let
8.5 val a' = Sign.base_name a;
8.6 val b' = Sign.base_name b;
8.7 - val cp = dynamic_thm thy ("cp_" ^ a' ^ "_" ^ b' ^ "_inst");
8.8 - val dj = dynamic_thm thy ("dj_" ^ b' ^ "_" ^ a');
8.9 + val cp = PureThy.get_thm thy ("cp_" ^ a' ^ "_" ^ b' ^ "_inst");
8.10 + val dj = PureThy.get_thm thy ("dj_" ^ b' ^ "_" ^ a');
8.11 val dj_cp' = [cp, dj] MRS dj_cp;
8.12 val cert = SOME o cterm_of thy
8.13 in
8.14 @@ -309,7 +309,7 @@
8.15 val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
8.16
8.17 val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
8.18 - val perm_fun_def = dynamic_thm thy2 "perm_fun_def";
8.19 + val perm_fun_def = PureThy.get_thm thy2 "perm_fun_def";
8.20
8.21 val unfolded_perm_eq_thms =
8.22 if length descr = length new_type_names then []
8.23 @@ -353,17 +353,17 @@
8.24 val _ = warning "perm_append_thms";
8.25
8.26 (*FIXME: these should be looked up statically*)
8.27 - val at_pt_inst = dynamic_thm thy2 "at_pt_inst";
8.28 - val pt2 = dynamic_thm thy2 "pt2";
8.29 + val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst";
8.30 + val pt2 = PureThy.get_thm thy2 "pt2";
8.31
8.32 val perm_append_thms = List.concat (map (fn a =>
8.33 let
8.34 val permT = mk_permT (Type (a, []));
8.35 val pi1 = Free ("pi1", permT);
8.36 val pi2 = Free ("pi2", permT);
8.37 - val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
8.38 + val pt_inst = PureThy.get_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
8.39 val pt2' = pt_inst RS pt2;
8.40 - val pt2_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a);
8.41 + val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a);
8.42 in List.take (map standard (split_conj_thm
8.43 (Goal.prove_global thy2 [] []
8.44 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
8.45 @@ -385,8 +385,8 @@
8.46
8.47 val _ = warning "perm_eq_thms";
8.48
8.49 - val pt3 = dynamic_thm thy2 "pt3";
8.50 - val pt3_rev = dynamic_thm thy2 "pt3_rev";
8.51 + val pt3 = PureThy.get_thm thy2 "pt3";
8.52 + val pt3_rev = PureThy.get_thm thy2 "pt3_rev";
8.53
8.54 val perm_eq_thms = List.concat (map (fn a =>
8.55 let
8.56 @@ -394,11 +394,11 @@
8.57 val pi1 = Free ("pi1", permT);
8.58 val pi2 = Free ("pi2", permT);
8.59 (*FIXME: not robust - better access these theorems using NominalData?*)
8.60 - val at_inst = dynamic_thm thy2 ("at_" ^ Sign.base_name a ^ "_inst");
8.61 - val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
8.62 + val at_inst = PureThy.get_thm thy2 ("at_" ^ Sign.base_name a ^ "_inst");
8.63 + val pt_inst = PureThy.get_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
8.64 val pt3' = pt_inst RS pt3;
8.65 val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
8.66 - val pt3_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a);
8.67 + val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a);
8.68 in List.take (map standard (split_conj_thm
8.69 (Goal.prove_global thy2 [] [] (Logic.mk_implies
8.70 (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
8.71 @@ -419,11 +419,11 @@
8.72
8.73 (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
8.74
8.75 - val cp1 = dynamic_thm thy2 "cp1";
8.76 - val dj_cp = dynamic_thm thy2 "dj_cp";
8.77 - val pt_perm_compose = dynamic_thm thy2 "pt_perm_compose";
8.78 - val pt_perm_compose_rev = dynamic_thm thy2 "pt_perm_compose_rev";
8.79 - val dj_perm_perm_forget = dynamic_thm thy2 "dj_perm_perm_forget";
8.80 + val cp1 = PureThy.get_thm thy2 "cp1";
8.81 + val dj_cp = PureThy.get_thm thy2 "dj_cp";
8.82 + val pt_perm_compose = PureThy.get_thm thy2 "pt_perm_compose";
8.83 + val pt_perm_compose_rev = PureThy.get_thm thy2 "pt_perm_compose_rev";
8.84 + val dj_perm_perm_forget = PureThy.get_thm thy2 "dj_perm_perm_forget";
8.85
8.86 fun composition_instance name1 name2 thy =
8.87 let
8.88 @@ -435,15 +435,15 @@
8.89 val augment = map_type_tfree
8.90 (fn (x, S) => TFree (x, cp_class :: S));
8.91 val Ts = map (augment o body_type) perm_types;
8.92 - val cp_inst = dynamic_thm thy ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst");
8.93 + val cp_inst = PureThy.get_thm thy ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst");
8.94 val simps = simpset_of thy addsimps (perm_fun_def ::
8.95 (if name1 <> name2 then
8.96 - let val dj = dynamic_thm thy ("dj_" ^ name2' ^ "_" ^ name1')
8.97 + let val dj = PureThy.get_thm thy ("dj_" ^ name2' ^ "_" ^ name1')
8.98 in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
8.99 else
8.100 let
8.101 - val at_inst = dynamic_thm thy ("at_" ^ name1' ^ "_inst");
8.102 - val pt_inst = dynamic_thm thy ("pt_" ^ name1' ^ "_inst");
8.103 + val at_inst = PureThy.get_thm thy ("at_" ^ name1' ^ "_inst");
8.104 + val pt_inst = PureThy.get_thm thy ("pt_" ^ name1' ^ "_inst");
8.105 in
8.106 [cp_inst RS cp1 RS sym,
8.107 at_inst RS (pt_inst RS pt_perm_compose) RS sym,
8.108 @@ -571,7 +571,7 @@
8.109
8.110 val _ = warning "proving closure under permutation...";
8.111
8.112 - val abs_perm = dynamic_thms thy4 "abs_perm";
8.113 + val abs_perm = PureThy.get_thms thy4 "abs_perm";
8.114
8.115 val perm_indnames' = List.mapPartial
8.116 (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
8.117 @@ -656,7 +656,7 @@
8.118 asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
8.119 asm_full_simp_tac (simpset_of thy addsimps
8.120 [Rep RS perm_closed RS Abs_inverse]) 1,
8.121 - asm_full_simp_tac (HOL_basic_ss addsimps [dynamic_thm thy
8.122 + asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
8.123 ("pt_" ^ Sign.base_name atom ^ "3")]) 1]) thy)
8.124 (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
8.125 new_type_names ~~ tyvars ~~ perm_closed_thms);
8.126 @@ -670,7 +670,7 @@
8.127 let
8.128 val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2;
8.129 val class = Sign.intern_class thy name;
8.130 - val cp1' = dynamic_thm thy (name ^ "_inst") RS cp1
8.131 + val cp1' = PureThy.get_thm thy (name ^ "_inst") RS cp1
8.132 in fold (fn ((((((Abs_inverse, Rep),
8.133 perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
8.134 AxClass.prove_arity
8.135 @@ -920,8 +920,8 @@
8.136 (** prove injectivity of constructors **)
8.137
8.138 val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
8.139 - val alpha = dynamic_thms thy8 "alpha";
8.140 - val abs_fresh = dynamic_thms thy8 "abs_fresh";
8.141 + val alpha = PureThy.get_thms thy8 "alpha";
8.142 + val abs_fresh = PureThy.get_thms thy8 "abs_fresh";
8.143
8.144 val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
8.145 let val T = nth_dtyp' i
8.146 @@ -1066,8 +1066,8 @@
8.147
8.148 val indnames = DatatypeProp.make_tnames recTs;
8.149
8.150 - val abs_supp = dynamic_thms thy8 "abs_supp";
8.151 - val supp_atm = dynamic_thms thy8 "supp_atm";
8.152 + val abs_supp = PureThy.get_thms thy8 "abs_supp";
8.153 + val supp_atm = PureThy.get_thms thy8 "supp_atm";
8.154
8.155 val finite_supp_thms = map (fn atom =>
8.156 let val atomT = Type (atom, [])
8.157 @@ -1080,7 +1080,7 @@
8.158 (fn _ => indtac dt_induct indnames 1 THEN
8.159 ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
8.160 (abs_supp @ supp_atm @
8.161 - dynamic_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @
8.162 + PureThy.get_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @
8.163 List.concat supp_thms))))),
8.164 length new_type_names))
8.165 end) atoms;
8.166 @@ -1207,23 +1207,23 @@
8.167 (descr'' ~~ recTs ~~ tnames)));
8.168
8.169 val fin_set_supp = map (fn Type (s, _) =>
8.170 - dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
8.171 + PureThy.get_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
8.172 at_fin_set_supp) dt_atomTs;
8.173 val fin_set_fresh = map (fn Type (s, _) =>
8.174 - dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
8.175 + PureThy.get_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
8.176 at_fin_set_fresh) dt_atomTs;
8.177 val pt1_atoms = map (fn Type (s, _) =>
8.178 - dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs;
8.179 + PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs;
8.180 val pt2_atoms = map (fn Type (s, _) =>
8.181 - dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs;
8.182 - val exists_fresh' = dynamic_thms thy9 "exists_fresh'";
8.183 - val fs_atoms = dynamic_thms thy9 "fin_supp";
8.184 - val abs_supp = dynamic_thms thy9 "abs_supp";
8.185 - val perm_fresh_fresh = dynamic_thms thy9 "perm_fresh_fresh";
8.186 - val calc_atm = dynamic_thms thy9 "calc_atm";
8.187 - val fresh_atm = dynamic_thms thy9 "fresh_atm";
8.188 - val fresh_left = dynamic_thms thy9 "fresh_left";
8.189 - val perm_swap = dynamic_thms thy9 "perm_swap";
8.190 + PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs;
8.191 + val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
8.192 + val fs_atoms = PureThy.get_thms thy9 "fin_supp";
8.193 + val abs_supp = PureThy.get_thms thy9 "abs_supp";
8.194 + val perm_fresh_fresh = PureThy.get_thms thy9 "perm_fresh_fresh";
8.195 + val calc_atm = PureThy.get_thms thy9 "calc_atm";
8.196 + val fresh_atm = PureThy.get_thms thy9 "fresh_atm";
8.197 + val fresh_left = PureThy.get_thms thy9 "fresh_left";
8.198 + val perm_swap = PureThy.get_thms thy9 "perm_swap";
8.199
8.200 fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
8.201 let
8.202 @@ -1496,8 +1496,8 @@
8.203
8.204 (** equivariance **)
8.205
8.206 - val fresh_bij = dynamic_thms thy11 "fresh_bij";
8.207 - val perm_bij = dynamic_thms thy11 "perm_bij";
8.208 + val fresh_bij = PureThy.get_thms thy11 "fresh_bij";
8.209 + val perm_bij = PureThy.get_thms thy11 "perm_bij";
8.210
8.211 val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT =>
8.212 let
8.213 @@ -1535,7 +1535,7 @@
8.214 val rec_fin_supp_thms = map (fn aT =>
8.215 let
8.216 val name = Sign.base_name (fst (dest_Type aT));
8.217 - val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1");
8.218 + val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
8.219 val aset = HOLogic.mk_setT aT;
8.220 val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
8.221 val fins = map (fn (f, T) => HOLogic.mk_Trueprop
8.222 @@ -1568,7 +1568,7 @@
8.223 val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
8.224 let
8.225 val name = Sign.base_name (fst (dest_Type aT));
8.226 - val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1");
8.227 + val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
8.228 val a = Free ("a", aT);
8.229 val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
8.230 (fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts)
9.1 --- a/src/HOL/Nominal/nominal_permeq.ML Wed Mar 19 22:50:42 2008 +0100
9.2 +++ b/src/HOL/Nominal/nominal_permeq.ML Thu Mar 20 00:20:44 2008 +0100
9.3 @@ -71,8 +71,8 @@
9.4 val supports_fresh_rule = @{thm "supports_fresh"};
9.5
9.6 (* pulls out dynamically a thm via the proof state *)
9.7 -fun global_thms st name = PureThy.get_thms (theory_of_thm st) (Facts.Named (name, NONE));
9.8 -fun global_thm st name = PureThy.get_thm (theory_of_thm st) (Facts.Named (name, NONE));
9.9 +fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) name;
9.10 +fun dynamic_thm st name = PureThy.get_thm (theory_of_thm st) name;
9.11
9.12
9.13 (* needed in the process of fully simplifying permutations *)
9.14 @@ -111,8 +111,8 @@
9.15 (if (applicable_app f) then
9.16 let
9.17 val name = Sign.base_name n
9.18 - val at_inst = dynamic_thm sg ("at_" ^ name ^ "_inst")
9.19 - val pt_inst = dynamic_thm sg ("pt_" ^ name ^ "_inst")
9.20 + val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst")
9.21 + val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst")
9.22 in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
9.23 else NONE)
9.24 | _ => NONE
9.25 @@ -146,7 +146,7 @@
9.26 ("general simplification of permutations", fn st =>
9.27 let
9.28 val ss' = Simplifier.theory_context (theory_of_thm st) ss
9.29 - addsimps ((List.concat (map (global_thms st) dyn_thms))@eqvt_thms)
9.30 + addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
9.31 delcongs weak_congs
9.32 addcongs strong_congs
9.33 addsimprocs [perm_simproc_fun, perm_simproc_app]
9.34 @@ -198,13 +198,13 @@
9.35 SOME (Drule.instantiate'
9.36 [SOME (ctyp_of sg (fastype_of t))]
9.37 [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
9.38 - (mk_meta_eq ([dynamic_thm sg ("pt_"^tname'^"_inst"),
9.39 - dynamic_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
9.40 + (mk_meta_eq ([PureThy.get_thm sg ("pt_"^tname'^"_inst"),
9.41 + PureThy.get_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
9.42 else
9.43 SOME (Drule.instantiate'
9.44 [SOME (ctyp_of sg (fastype_of t))]
9.45 [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
9.46 - (mk_meta_eq (dynamic_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS
9.47 + (mk_meta_eq (PureThy.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS
9.48 cp1_aux)))
9.49 else NONE
9.50 end
9.51 @@ -307,7 +307,7 @@
9.52 Logic.strip_assums_concl (hd (prems_of supports_rule'));
9.53 val supports_rule'' = Drule.cterm_instantiate
9.54 [(cert (head_of S), cert s')] supports_rule'
9.55 - val fin_supp = global_thms st ("fin_supp")
9.56 + val fin_supp = dynamic_thms st ("fin_supp")
9.57 val ss' = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
9.58 in
9.59 (tactical ("guessing of the right supports-set",
9.60 @@ -326,8 +326,8 @@
9.61 fun fresh_guess_tac tactical ss i st =
9.62 let
9.63 val goal = List.nth(cprems_of st, i-1)
9.64 - val fin_supp = global_thms st ("fin_supp")
9.65 - val fresh_atm = global_thms st ("fresh_atm")
9.66 + val fin_supp = dynamic_thms st ("fin_supp")
9.67 + val fresh_atm = dynamic_thms st ("fresh_atm")
9.68 val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
9.69 val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
9.70 in
10.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML Wed Mar 19 22:50:42 2008 +0100
10.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Mar 20 00:20:44 2008 +0100
10.3 @@ -10,9 +10,6 @@
10.4 respectively the lemma from the data-slot.
10.5 *)
10.6
10.7 -fun dynamic_thm thy name = PureThy.get_thm thy (Facts.Named (name, NONE));
10.8 -fun dynamic_thms thy name = PureThy.get_thms thy (Facts.Named (name, NONE));
10.9 -
10.10 signature NOMINAL_THMDECLS =
10.11 sig
10.12 val print_data: Proof.context -> unit
10.13 @@ -83,7 +80,7 @@
10.14 let
10.15 val mypi = Thm.cterm_of ctx (Var (pi,typi))
10.16 val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
10.17 - val perm_pi_simp = dynamic_thms ctx "perm_pi_simp"
10.18 + val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
10.19 in
10.20 EVERY [tactic ("iffI applied",rtac iffI 1),
10.21 tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)),
11.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML Wed Mar 19 22:50:42 2008 +0100
11.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Thu Mar 20 00:20:44 2008 +0100
11.3 @@ -339,7 +339,7 @@
11.4
11.5 fun neq_x_y ctxt x y name =
11.6 (let
11.7 - val dist_thm = the (try (ProofContext.get_thm ctxt) (Facts.Named (name, NONE)));
11.8 + val dist_thm = the (try (ProofContext.get_thm ctxt) name);
11.9 val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
11.10 val tree = term_of ctree;
11.11 val x_path = the (find_tree x tree);
12.1 --- a/src/HOL/Statespace/state_space.ML Wed Mar 19 22:50:42 2008 +0100
12.2 +++ b/src/HOL/Statespace/state_space.ML Thu Mar 20 00:20:44 2008 +0100
12.3 @@ -270,7 +270,7 @@
12.4
12.5 fun solve_tac ctxt (_,i) st =
12.6 let
12.7 - val distinct_thm = ProofContext.get_thm ctxt (Facts.Named (dist_thm_name, NONE));
12.8 + val distinct_thm = ProofContext.get_thm ctxt dist_thm_name;
12.9 val goal = List.nth (cprems_of st,i-1);
12.10 val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
12.11 in EVERY [rtac rule i] st
13.1 --- a/src/HOL/Tools/datatype_package.ML Wed Mar 19 22:50:42 2008 +0100
13.2 +++ b/src/HOL/Tools/datatype_package.ML Thu Mar 20 00:20:44 2008 +0100
13.3 @@ -391,7 +391,7 @@
13.4 | ManyConstrs (thm, simpset) =>
13.5 let
13.6 val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
13.7 - map (fn a => get_thm (ThyInfo.the_theory "Datatype" thy) (Facts.Named (a, NONE)))
13.8 + map (PureThy.get_thm (ThyInfo.the_theory "Datatype" thy))
13.9 ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
13.10 in
13.11 Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
14.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Mar 19 22:50:42 2008 +0100
14.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Mar 20 00:20:44 2008 +0100
14.3 @@ -57,11 +57,10 @@
14.4
14.5 val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
14.6 In0_eq, In1_eq, In0_not_In1, In1_not_In0,
14.7 - Lim_inject, Suml_inject, Sumr_inject] =
14.8 - map (fn a => get_thm Datatype_thy (Facts.Named (a, NONE)))
14.9 - ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
14.10 - "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
14.11 - "Lim_inject", "Suml_inject", "Sumr_inject"];
14.12 + Lim_inject, Suml_inject, Sumr_inject] = map (PureThy.get_thm Datatype_thy)
14.13 + ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
14.14 + "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
14.15 + "Lim_inject", "Suml_inject", "Sumr_inject"];
14.16
14.17 val descr' = List.concat descr;
14.18
15.1 --- a/src/HOL/Tools/inductive_realizer.ML Wed Mar 19 22:50:42 2008 +0100
15.2 +++ b/src/HOL/Tools/inductive_realizer.ML Thu Mar 20 00:20:44 2008 +0100
15.3 @@ -276,7 +276,7 @@
15.4 fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
15.5 let
15.6 val qualifier = NameSpace.qualifier (name_of_thm induct);
15.7 - val inducts = PureThy.get_thms thy (Facts.Named (NameSpace.qualified qualifier "inducts", NONE));
15.8 + val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts");
15.9 val iTs = term_tvars (prop_of (hd intrs));
15.10 val ar = length vs + length iTs;
15.11 val params = InductivePackage.params_of raw_induct;
16.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Wed Mar 19 22:50:42 2008 +0100
16.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Thu Mar 20 00:20:44 2008 +0100
16.3 @@ -98,7 +98,7 @@
16.4 fun unqualify s = implode(rev(afpl(rev(explode s))));
16.5 val q_atypstr = act_name thy atyp;
16.6 val uq_atypstr = unqualify q_atypstr;
16.7 -val prem = prems_of (PureThy.get_thm thy (Facts.Named (uq_atypstr ^ ".induct", NONE)));
16.8 +val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
16.9 in
16.10 extract_constrs thy prem
16.11 handle malformed =>
16.12 @@ -284,7 +284,7 @@
16.13 let
16.14 fun left_of (( _ $ left) $ _) = left |
16.15 left_of _ = raise malformed;
16.16 -val aut_def = concl_of (PureThy.get_thm thy (Facts.Named (aut_name ^ "_def", NONE)));
16.17 +val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
16.18 in
16.19 (#T(rep_cterm(cterm_of thy (left_of aut_def))))
16.20 handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
17.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML Wed Mar 19 22:50:42 2008 +0100
17.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Thu Mar 20 00:20:44 2008 +0100
17.3 @@ -126,7 +126,7 @@
17.4 (* ----- getting the axioms and definitions --------------------------------- *)
17.5
17.6 local
17.7 - fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
17.8 + fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
17.9 in
17.10 val ax_abs_iso = ga "abs_iso" dname;
17.11 val ax_rep_iso = ga "rep_iso" dname;
17.12 @@ -612,7 +612,7 @@
17.13 (* ----- getting the composite axiom and definitions ------------------------ *)
17.14
17.15 local
17.16 - fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
17.17 + fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
17.18 in
17.19 val axs_reach = map (ga "reach" ) dnames;
17.20 val axs_take_def = map (ga "take_def" ) dnames;
17.21 @@ -622,8 +622,8 @@
17.22 end;
17.23
17.24 local
17.25 - fun gt s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
17.26 - fun gts s dn = PureThy.get_thms thy (Facts.Named (dn ^ "." ^ s, NONE));
17.27 + fun gt s dn = PureThy.get_thm thy (dn ^ "." ^ s);
17.28 + fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
17.29 in
17.30 val cases = map (gt "casedist" ) dnames;
17.31 val con_rews = maps (gts "con_rews" ) dnames;
18.1 --- a/src/HOLCF/Tools/fixrec_package.ML Wed Mar 19 22:50:42 2008 +0100
18.2 +++ b/src/HOLCF/Tools/fixrec_package.ML Thu Mar 20 00:20:44 2008 +0100
18.3 @@ -267,7 +267,7 @@
18.4 val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
18.5 val cname = case chead_of t of Const(c,_) => c | _ =>
18.6 fixrec_err "function is not declared as constant in theory";
18.7 - val unfold_thm = PureThy.get_thm thy (Facts.Named (cname^"_unfold", NONE));
18.8 + val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
18.9 val simp = Goal.prove_global thy [] [] eq
18.10 (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
18.11 in simp end;
19.1 --- a/src/Pure/Proof/extraction.ML Wed Mar 19 22:50:42 2008 +0100
19.2 +++ b/src/Pure/Proof/extraction.ML Thu Mar 20 00:20:44 2008 +0100
19.3 @@ -765,8 +765,7 @@
19.4 K.thy_decl
19.5 (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
19.6 (fn xs => Toplevel.theory (fn thy => add_realizers
19.7 - (map (fn (((a, vs), s1), s2) =>
19.8 - (PureThy.get_thm thy (Facts.Named (a, NONE)), (vs, s1, s2))) xs) thy)));
19.9 + (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
19.10
19.11 val _ =
19.12 OuterSyntax.command "realizability"
19.13 @@ -781,7 +780,7 @@
19.14 val _ =
19.15 OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
19.16 (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
19.17 - extract (map (fn (a, vs) => (PureThy.get_thm thy (Facts.Named (a, NONE)), vs)) xs) thy)));
19.18 + extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
19.19
19.20 val etype_of = etype_of o add_syntax;
19.21
20.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Mar 19 22:50:42 2008 +0100
20.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 20 00:20:44 2008 +0100
20.3 @@ -712,7 +712,7 @@
20.4 What we want is mapping onto simple PGIP name/context model. *)
20.5 val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *)
20.6 val thy = Context.theory_of_proof ctx
20.7 - val ths = [PureThy.get_thm thy (Facts.Named (thmname, NONE))]
20.8 + val ths = [PureThy.get_thm thy thmname]
20.9 val deps = filter_out (equal "")
20.10 (Symtab.keys (fold Proofterm.thms_of_proof
20.11 (map Thm.proof_of ths) Symtab.empty))
20.12 @@ -764,7 +764,7 @@
20.13 [] (* asms *)
20.14 th))
20.15
20.16 - fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Facts.Named (name, NONE)))
20.17 + fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
20.18
20.19 val string_of_thy = Output.output o
20.20 Pretty.string_of o (ProofDisplay.pretty_full_theory false)
21.1 --- a/src/Tools/Compute_Oracle/linker.ML Wed Mar 19 22:50:42 2008 +0100
21.2 +++ b/src/Tools/Compute_Oracle/linker.ML Thu Mar 20 00:20:44 2008 +0100
21.3 @@ -192,7 +192,7 @@
21.4 fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
21.5
21.6 local
21.7 - fun get_thm thmname = PureThy.get_thm (theory "Main") (Facts.Named (thmname, NONE))
21.8 + fun get_thm thmname = PureThy.get_thm (theory "Main") thmname
21.9 val eq_th = get_thm "HOL.eq_reflection"
21.10 in
21.11 fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)