diff -r 0cbcdfd9e527 -r d5d6111761a6 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Apr 30 23:43:09 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Apr 30 23:53:37 2010 +0200
@@ -152,7 +152,8 @@
       in
         case map_filter (fn th'' =>
             SOME (th'', singleton
-              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
+              (Variable.trade (K (fn [th'''] => [th''' RS th']))
+                (Variable.global_thm_context th'')) th'')
           handle THM _ => NONE) thms of
             [] => NONE
           | thps =>