changeset 13418 | 7c0ba9dba978 |
parent 13409 | d4ea094c650e |
child 13422 | af9bc8d87a75 |
--- a/src/ZF/Constructible/Rec_Separation.thy Wed Jul 24 16:16:44 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Wed Jul 24 17:59:12 2002 +0200 @@ -1114,7 +1114,7 @@ val m_eclose = [eclose_replacement1, eclose_replacement2]; fun eclose_L th = - kill_flex_triv_prems (m_eclose MRS (wfrank_L th)); + kill_flex_triv_prems (m_eclose MRS (datatypes_L th)); bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed")); bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs"));