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