Adapted to modified interface of PureThy.get_thm(s).
authorberghofe
Mon Jan 24 18:16:57 2005 +0100 (2005-01-24 ago)
changeset 1546395cb3eb74307
parent 15462 b4208fbf9439
child 15464 02cc838b64ca
Adapted to modified interface of PureThy.get_thm(s).
src/HOL/Algebra/ringsimp.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Library/word_setup.ML
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Algebra/ringsimp.ML	Mon Jan 24 18:15:19 2005 +0100
     1.2 +++ b/src/HOL/Algebra/ringsimp.ML	Mon Jan 24 18:16:57 2005 +0100
     1.3 @@ -82,9 +82,9 @@
     1.4        ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^
     1.5         "\nCommutative rings in proof context: " ^ commas comm_rings);
     1.6      val simps =
     1.7 -      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules"))
     1.8 +      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules", None))
     1.9          non_comm_rings) @
    1.10 -      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules"))
    1.11 +      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules", None))
    1.12          comm_rings);
    1.13    in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
    1.14    end;
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Jan 24 18:15:19 2005 +0100
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Jan 24 18:16:57 2005 +0100
     2.3 @@ -1236,10 +1236,10 @@
     2.4  	    Some (Some thmname) =>
     2.5  	    let
     2.6  		val _ = message ("Looking for " ^ thmname)
     2.7 -		val th1 = (Some (transform_error (PureThy.get_thm thy) thmname)
     2.8 +		val th1 = (Some (transform_error (PureThy.get_thm thy) (thmname, None))
     2.9  			   handle ERROR_MESSAGE _ =>
    2.10  				  (case split_name thmname of
    2.11 -				       Some (listname,idx) => (Some (nth_elem(idx-1,PureThy.get_thms thy listname))
    2.12 +				       Some (listname,idx) => (Some (nth_elem(idx-1,PureThy.get_thms thy (listname, None)))
    2.13  							       handle _ => None)
    2.14  				     | None => None))
    2.15  	    in
     3.1 --- a/src/HOL/Library/word_setup.ML	Mon Jan 24 18:15:19 2005 +0100
     3.2 +++ b/src/HOL/Library/word_setup.ML	Mon Jan 24 18:16:57 2005 +0100
     3.3 @@ -24,7 +24,7 @@
     3.4      fun add_word thy =
     3.5  	let
     3.6   (*lcp**	    val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
     3.7 -	    val fast2_th = PureThy.get_thm thy "Word.fast_bv_to_nat_def"
     3.8 +	    val fast2_th = PureThy.get_thm thy ("Word.fast_bv_to_nat_def", None)
     3.9   (*lcp**	    fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
    3.10  		if num_is_usable t
    3.11  		then Some (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
     4.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Jan 24 18:15:19 2005 +0100
     4.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Jan 24 18:16:57 2005 +0100
     4.3 @@ -51,7 +51,7 @@
     4.4        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
     4.5         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
     4.6    val add_inductive: bool -> bool -> string list ->
     4.7 -    ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
     4.8 +    ((bstring * string) * Args.src list) list -> (thmref * Args.src list) list ->
     4.9      theory -> theory *
    4.10        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    4.11         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    4.12 @@ -617,11 +617,11 @@
    4.13      val sign = Theory.sign_of thy;
    4.14  
    4.15      val sum_case_rewrites =
    4.16 -      (if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy "sum.cases"
    4.17 +      (if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy ("sum.cases", None)
    4.18          else
    4.19            (case ThyInfo.lookup_theory "Datatype" of
    4.20              None => []
    4.21 -          | Some thy' => PureThy.get_thms thy' "sum.cases")) |> map mk_meta_eq;
    4.22 +          | Some thy' => PureThy.get_thms thy' ("sum.cases", None))) |> map mk_meta_eq;
    4.23  
    4.24      val (preds, ind_prems, mutual_ind_concl, factors) =
    4.25        mk_indrule cs cTs params intr_ts;