484 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
484 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
485 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
485 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
486 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
486 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
487 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} |
487 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} |
488 val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi) |
488 val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi) |
489 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
489 val ts = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} te |
490 val (insp, inst) = |
490 val (insp, inst) = |
491 if ty_c = ty_d |
491 if ty_c = ty_d |
492 then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm) |
492 then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm) |
493 else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
493 else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
494 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
494 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |