src/HOL/Tools/meson.ML

--- a/src/HOL/Tools/meson.ML	Sat Mar 20 02:23:41 2010 +0100
+++ b/src/HOL/Tools/meson.ML	Sat Mar 20 17:33:11 2010 +0100
@@ -667,7 +667,7 @@
 fun make_meta_clause th =
   let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
   in  
-      (zero_var_indexes o Thm.varifyT o thaw 0 o 
+      (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
        negated_asm_of_head o make_horn resolution_clause_rules) fth
   end;