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