1.1 --- a/src/HOL/Tools/meson.ML	Wed Jun 11 18:01:36 2008 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Jun 11 18:02:00 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 = read_instantiate [("R","False")] notE;
     1.8 +val notEfalse = Drule.read_instantiate [("R","False")] notE;
     1.9  val notEfalse' = rotate_prems 1 notEfalse;
    1.10  
    1.11  fun negated_asm_of_head th =