src/HOL/Library/Efficient_Nat.thy
changeset 36603 d5d6111761a6
parent 36176 3fe7e97ccca8
child 37050 4a021f6be77c
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Apr 30 23:43:09 2010 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Apr 30 23:53:37 2010 +0200
     1.3 @@ -152,7 +152,8 @@
     1.4        in
     1.5          case map_filter (fn th'' =>
     1.6              SOME (th'', singleton
     1.7 -              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
     1.8 +              (Variable.trade (K (fn [th'''] => [th''' RS th']))
     1.9 +                (Variable.global_thm_context th'')) th'')
    1.10            handle THM _ => NONE) thms of
    1.11              [] => NONE
    1.12            | thps =>