--- a/src/HOL/Tools/meson.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Tools/meson.ML Mon Jun 16 22:13:39 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 = RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE;
+val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
val notEfalse' = rotate_prems 1 notEfalse;
fun negated_asm_of_head th =