--- a/src/HOL/Library/Code_Abstract_Nat.thy Sun Dec 21 16:27:22 2014 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Sun Dec 21 19:14:16 2014 +0100
@@ -86,7 +86,7 @@
case map_filter (fn thm'' =>
SOME (thm'', singleton
(Variable.trade (K (fn [thm'''] => [thm''' RS thm']))
- (Variable.global_thm_context thm'')) thm'')
+ (Variable.declare_thm thm'' ctxt)) thm'')
handle THM _ => NONE) thms of
[] => NONE
| thmps =>
@@ -95,13 +95,13 @@
end
in get_first mk_thms eqs end;
-fun eqn_suc_base_preproc thy thms =
+fun eqn_suc_base_preproc ctxt thms =
let
val dest = fst o Logic.dest_equals o prop_of;
val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
in
if forall (can dest) thms andalso exists (contains_suc o dest) thms
- then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
+ then thms |> perhaps_loop (remove_suc ctxt) |> (Option.map o map) Drule.zero_var_indexes
else NONE
end;
--- a/src/HOL/Tools/simpdata.ML Sun Dec 21 16:27:22 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML Sun Dec 21 19:14:16 2014 +0100
@@ -87,14 +87,15 @@
else error "Conclusion of congruence rules must be =-equality"
end);
-fun mk_atomize pairs =
+fun mk_atomize ctxt pairs =
let
fun atoms thm =
let
fun res th = map (fn rl => th RS rl); (*exception THM*)
+ val thm_ctxt = Variable.declare_thm thm ctxt;
fun res_fixed rls =
if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls
- else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm];
+ else Variable.trade (K (fn [thm'] => res thm' rls)) thm_ctxt [thm];
in
case concl_of thm
of Const (@{const_name Trueprop}, _) $ p => (case head_of p
@@ -106,8 +107,8 @@
end;
in atoms end;
-fun mksimps pairs (_: Proof.context) =
- map_filter (try mk_eq) o mk_atomize pairs o gen_all;
+fun mksimps pairs ctxt =
+ map_filter (try mk_eq) o mk_atomize ctxt pairs o gen_all;
val simp_legacy_precond =
Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false)