negate_nead (???) changed to negated_asm_of_head
authorpaulson
Fri, 21 Jan 2005 13:52:57 +0100
changeset 15448 fb7b8313a20d
parent 15447 177ffdbabf80
child 15449 a27c81bd838d
negate_nead (???) changed to negated_asm_of_head
src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Jan 21 13:52:09 2005 +0100
+++ b/src/HOL/Tools/meson.ML	Fri Jan 21 13:52:57 2005 +0100
@@ -356,11 +356,11 @@
 val notEfalse = read_instantiate [("R","False")] notE;
 val notEfalse' = rotate_prems 1 notEfalse;
 
-fun negate_nead th = 
+fun negated_asm_of_head th = 
     th RS notEfalse handle THM _ => th RS notEfalse';
 
 (*Converting one clause*)
-fun make_meta_clause th = negate_nead (make_horn resolution_clause_rules th);
+fun make_meta_clause th = negated_asm_of_head (make_horn resolution_clause_rules th);
 
 fun make_meta_clauses ths =
     name_thms "MClause#"