changeset 60801 | 7664e0916eec |
parent 60784 | 4f590c08fd5d |
child 60918 | 4ceef1592e8c |
child 60924 | 610794dff23c |
--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Jul 27 16:35:12 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Jul 27 17:44:55 2015 +0200 @@ -1251,7 +1251,7 @@ map Bound (live - 1 downto 0)) $ Bound live)); val cts = [NONE, SOME (Thm.cterm_of lthy tinst)]; in - Drule.instantiate' cTs cts @{thm surj_imp_ordLeq} + Thm.instantiate' cTs cts @{thm surj_imp_ordLeq} end); val bd = mk_cexp (if live = 0 then ctwo