Adapted to modified interface of PureThy.get_thm(s).
--- a/src/HOL/Algebra/ringsimp.ML Mon Jan 24 18:15:19 2005 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Mon Jan 24 18:16:57 2005 +0100
@@ -82,9 +82,9 @@
("Non-commutative rings in proof context: " ^ commas non_comm_rings ^
"\nCommutative rings in proof context: " ^ commas comm_rings);
val simps =
- flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules"))
+ flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules", None))
non_comm_rings) @
- flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules"))
+ flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules", None))
comm_rings);
in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
end;
--- a/src/HOL/Import/proof_kernel.ML Mon Jan 24 18:15:19 2005 +0100
+++ b/src/HOL/Import/proof_kernel.ML Mon Jan 24 18:16:57 2005 +0100
@@ -1236,10 +1236,10 @@
Some (Some thmname) =>
let
val _ = message ("Looking for " ^ thmname)
- val th1 = (Some (transform_error (PureThy.get_thm thy) thmname)
+ val th1 = (Some (transform_error (PureThy.get_thm thy) (thmname, None))
handle ERROR_MESSAGE _ =>
(case split_name thmname of
- Some (listname,idx) => (Some (nth_elem(idx-1,PureThy.get_thms thy listname))
+ Some (listname,idx) => (Some (nth_elem(idx-1,PureThy.get_thms thy (listname, None)))
handle _ => None)
| None => None))
in
--- a/src/HOL/Library/word_setup.ML Mon Jan 24 18:15:19 2005 +0100
+++ b/src/HOL/Library/word_setup.ML Mon Jan 24 18:16:57 2005 +0100
@@ -24,7 +24,7 @@
fun add_word thy =
let
(*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
- val fast2_th = PureThy.get_thm thy "Word.fast_bv_to_nat_def"
+ val fast2_th = PureThy.get_thm thy ("Word.fast_bv_to_nat_def", None)
(*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
if num_is_usable t
then Some (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
--- a/src/HOL/Tools/inductive_package.ML Mon Jan 24 18:15:19 2005 +0100
+++ b/src/HOL/Tools/inductive_package.ML Mon Jan 24 18:16:57 2005 +0100
@@ -51,7 +51,7 @@
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
val add_inductive: bool -> bool -> string list ->
- ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
+ ((bstring * string) * Args.src list) list -> (thmref * Args.src list) list ->
theory -> theory *
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
@@ -617,11 +617,11 @@
val sign = Theory.sign_of thy;
val sum_case_rewrites =
- (if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy "sum.cases"
+ (if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy ("sum.cases", None)
else
(case ThyInfo.lookup_theory "Datatype" of
None => []
- | Some thy' => PureThy.get_thms thy' "sum.cases")) |> map mk_meta_eq;
+ | Some thy' => PureThy.get_thms thy' ("sum.cases", None))) |> map mk_meta_eq;
val (preds, ind_prems, mutual_ind_concl, factors) =
mk_indrule cs cTs params intr_ts;