# HG changeset patch
# User paulson
# Date 1176379127 -7200
# Node ID 197f6c4ff9a5a15bf8414346d3bdb9e50213fa99
# Parent  8a70bc64483351002516b17b26db18c73cf573f2
Zero variable indexes in clauses

diff -r 8a70bc644833 -r 197f6c4ff9a5 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#"