1.1 --- a/src/HOL/Tools/meson.ML Mon Jun 16 17:54:42 2008 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Mon Jun 16 17:54:43 2008 +0200
1.3 @@ -646,7 +646,7 @@
1.4 (*Rules to convert the head literal into a negated assumption. If the head
1.5 literal is already negated, then using notEfalse instead of notEfalse'
1.6 prevents a double negation.*)
1.7 -val notEfalse = Drule.read_instantiate [("R","False")] notE;
1.8 +val notEfalse = RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE;
1.9 val notEfalse' = rotate_prems 1 notEfalse;
1.10
1.11 fun negated_asm_of_head th =