src/HOL/Tools/meson.ML

--- a/src/HOL/Tools/meson.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/meson.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -665,7 +665,7 @@
 
 (*Converting one theorem from a disjunction to a meta-level clause*)
 fun make_meta_clause th =
-  let val (fth,thaw) = Drule.freeze_thaw_robust th
+  let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
   in  
       (zero_var_indexes o Thm.varifyT o thaw 0 o 
        negated_asm_of_head o make_horn resolution_clause_rules) fth