src/HOL/Tools/meson.ML

--- a/src/HOL/Tools/meson.ML	Thu Apr 12 13:58:02 2007 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Apr 12 13:58:47 2007 +0200
@@ -631,8 +631,8 @@
     th RS notEfalse handle THM _ => th RS notEfalse';
 
 (*Converting one clause*)
-fun make_meta_clause th = 
-  negated_asm_of_head (make_horn resolution_clause_rules th);
+val make_meta_clause = 
+  zero_var_indexes o negated_asm_of_head o make_horn resolution_clause_rules;
   
 fun make_meta_clauses ths =
     name_thms "MClause#"