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;