replaced obsolete standard/freeze_all by Variable.trade;

--- a/src/HOL/Library/EfficientNat.thy	Wed Aug 02 22:26:37 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Wed Aug 02 22:26:39 2006 +0200
@@ -181,7 +181,8 @@
                Suc_if_eq')) (Thm.forall_intr cv' th)
       in
         case List.mapPartial (fn th'' =>
-            SOME (th'', standard (Drule.freeze_all th'' RS th'))
+            SOME (th'', singleton
+              (Variable.trade (Variable.thm_context th'') (fn [th'''] => [th''' RS th'])) th'')
           handle THM _ => NONE) thms of
             [] => NONE
           | thps =>