Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Efficient_Nat.thy
changeset 36603 d5d6111761a6
parent 36176 3fe7e97ccca8
child 37050 4a021f6be77c 
--- 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 =>
isabelle