src/HOL/Tools/Meson/meson.ML
changeset 60801 7664e0916eec
parent 60781 2da59cdf531c
child 61268 abe08fb15a12
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon Jul 27 16:35:12 2015 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Jul 27 17:44:55 2015 +0200
     1.3 @@ -173,7 +173,7 @@
     1.4      let
     1.5        val cc = Thm.cterm_of ctxt c
     1.6        val ct = Thm.dest_arg (Thm.cprop_of th)
     1.7 -    in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
     1.8 +    in resolve_tac ctxt [th] i (Thm.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
     1.9    | _ => resolve_tac ctxt [th] i st
    1.10  
    1.11  (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,