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#"