src/HOL/Tools/Meson/meson.ML

--- a/src/HOL/Tools/Meson/meson.ML	Mon Mar 19 20:32:57 2012 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Mon Mar 19 21:10:33 2012 +0100
@@ -752,7 +752,7 @@
 
 (*Converting one theorem from a disjunction to a meta-level clause*)
 fun make_meta_clause th =
-  let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
+  let val (fth,thaw) = Misc_Legacy.freeze_thaw_robust th
   in  
       (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
        negated_asm_of_head o make_horn resolution_clause_rules) fth