--- a/src/HOL/Tools/meson.ML Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOL/Tools/meson.ML Wed Jun 11 18:02:00 2008 +0200
@@ -646,7 +646,7 @@
(*Rules to convert the head literal into a negated assumption. If the head
literal is already negated, then using notEfalse instead of notEfalse'
prevents a double negation.*)
-val notEfalse = read_instantiate [("R","False")] notE;
+val notEfalse = Drule.read_instantiate [("R","False")] notE;
val notEfalse' = rotate_prems 1 notEfalse;
fun negated_asm_of_head th =