diff -r 0cbcdfd9e527 -r d5d6111761a6 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Fri Apr 30 23:43:09 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML	Fri Apr 30 23:53:37 2010 +0200
@@ -95,7 +95,7 @@
         fun res th = map (fn rl => th RS rl);   (*exception THM*)
         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.thm_context thm) [thm];
+          else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm];
       in
         case concl_of thm
           of Const (@{const_name Trueprop}, _) $ p => (case head_of p