570 val absrep_trm = quot_thm_abs quot_thm |
570 val absrep_trm = quot_thm_abs quot_thm |
571 val rty_forced = (domain_type o fastype_of) absrep_trm |
571 val rty_forced = (domain_type o fastype_of) absrep_trm |
572 val forced_rhs = force_rty_type lthy rty_forced rhs |
572 val forced_rhs = force_rty_type lthy rty_forced rhs |
573 val lhs = Free (Binding.name_of binding, qty) |
573 val lhs = Free (Binding.name_of binding, qty) |
574 val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs) |
574 val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs) |
575 val (_, prop') = Local_Defs.cert_def lthy prop |
575 val (_, prop') = Local_Defs.cert_def lthy (K []) prop |
576 val (_, newrhs) = Local_Defs.abs_def prop' |
576 val (_, newrhs) = Local_Defs.abs_def prop' |
577 val var = ((#notes config = false ? Binding.concealed) binding, mx) |
577 val var = ((#notes config = false ? Binding.concealed) binding, mx) |
578 val def_name = Thm.make_def_binding (#notes config) (#1 var) |
578 val def_name = Thm.make_def_binding (#notes config) (#1 var) |
579 |
579 |
580 val ((lift_const, (_ , def_thm)), lthy) = |
580 val ((lift_const, (_ , def_thm)), lthy) = |