--- 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