equal
deleted
inserted
replaced
930 val t_a = atomize_thm t; |
930 val t_a = atomize_thm t; |
931 val t_r = regularize t_a rty rel rel_eqv lthy; |
931 val t_r = regularize t_a rty rel rel_eqv lthy; |
932 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
932 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
933 val abs = findabs rty (prop_of t_a); |
933 val abs = findabs rty (prop_of t_a); |
934 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
934 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
935 fun simp_lam_prs lthy thm = |
935 val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t; |
936 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
|
937 handle _ => thm |
|
938 val t_l = simp_lam_prs lthy t_t; |
|
939 val t_a = simp_allex_prs lthy quot t_l; |
936 val t_a = simp_allex_prs lthy quot t_l; |
940 val t_defs_sym = add_lower_defs lthy t_defs; |
937 val t_defs_sym = add_lower_defs lthy t_defs; |
941 val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a; |
938 val t_d = repeat_eqsubst_thm lthy t_defs_sym t_a; |
942 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
939 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
943 in |
940 in |
944 ObjectLogic.rulify t_r |
941 ObjectLogic.rulify t_r |
945 end |
942 end |
946 *} |
943 *} |