src/HOL/Tools/Meson/meson_clausify.ML
changeset 60801 7664e0916eec
parent 60781 2da59cdf531c
child 61268 abe08fb15a12
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon Jul 27 16:35:12 2015 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Mon Jul 27 17:44:55 2015 +0200
     1.3 @@ -102,13 +102,13 @@
     1.4        val cxT = Thm.ctyp_of ctxt xT
     1.5        val cbodyT = Thm.ctyp_of ctxt bodyT
     1.6        fun makeK () =
     1.7 -        instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.cterm_of ctxt body)] @{thm abs_K}
     1.8 +        Thm.instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.cterm_of ctxt body)] @{thm abs_K}
     1.9    in
    1.10        case body of
    1.11            Const _ => makeK()
    1.12          | Free _ => makeK()
    1.13          | Var _ => makeK()  (*though Var isn't expected*)
    1.14 -        | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
    1.15 +        | Bound 0 => Thm.instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
    1.16          | rator$rand =>
    1.17              if Term.is_dependent rator then (*C or S*)
    1.18                 if Term.is_dependent rand then (*S*)