# HG changeset patch
# User wenzelm
# Date 1419185656 -3600
# Node ID ddc948e4ed098174961def5b6783ba9fa30bfe34
# Parent  a5094641da6ad61010d876f5362e26d52970d667
proper context;

diff -r a5094641da6a -r ddc948e4ed09 src/HOL/Library/Code_Abstract_Nat.thy
--- 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;
 
diff -r a5094641da6a -r ddc948e4ed09 src/HOL/Tools/simpdata.ML
--- 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)