# HG changeset patch
# User wenzelm
# Date 1332188715 -3600
# Node ID 6c2b7b0421b500af096b8513c70ccd0628b61db3
# Parent  c7a89ecbc71e74e9242529365ceb1a67a25174b7
updated Misc_Legacy.freeze_thaw;

diff -r c7a89ecbc71e -r 6c2b7b0421b5 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Mon Mar 19 21:16:19 2012 +0100
+++ b/src/HOL/Import/shuffler.ML	Mon Mar 19 21:25:15 2012 +0100
@@ -231,7 +231,7 @@
 fun eta_contract thy _ origt =
     let
         val (typet,Tinst) = freeze_thaw_term origt
-        val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
+        val (init,thaw) = Misc_Legacy.freeze_thaw (Thm.reflexive (cterm_of thy typet))
         val final = inst_tfrees thy Tinst o thaw
         val t = #1 (Logic.dest_equals (prop_of init))
         val _ =
@@ -282,7 +282,7 @@
 fun eta_expand thy _ origt =
     let
         val (typet,Tinst) = freeze_thaw_term origt
-        val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
+        val (init,thaw) = Misc_Legacy.freeze_thaw (Thm.reflexive (cterm_of thy typet))
         val final = inst_tfrees thy Tinst o thaw
         val t = #1 (Logic.dest_equals (prop_of init))
         val _ =