# HG changeset patch
# User paulson
# Date 1106311977 -3600
# Node ID fb7b8313a20d3aeff2db8b8c49a6ccf7a58e4b05
# Parent  177ffdbabf80b36bc8f908bd6a42110fd7ae4472
negate_nead (???) changed to negated_asm_of_head

diff -r 177ffdbabf80 -r fb7b8313a20d 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#"