Zero variable indexes in clauses
authorpaulson
Thu, 12 Apr 2007 13:58:47 +0200
changeset 22646 197f6c4ff9a5
parent 22645 8a70bc644833
child 22647 d920afb63323
Zero variable indexes in clauses
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#"