29 fun internalize_sort ctvar thm = |
29 fun internalize_sort ctvar thm = |
30 let |
30 let |
31 val thy = Thm.theory_of_thm thm; |
31 val thy = Thm.theory_of_thm thm; |
32 val tvar = Thm.typ_of ctvar; |
32 val tvar = Thm.typ_of ctvar; |
33 |
33 |
34 val {constraints = assms, outer_constraints = classes, ...} = |
34 val (ucontext, _) = Logic.unconstrainT [] (Thm.prop_of thm); |
35 Logic.unconstrainT [] (Thm.prop_of thm); |
|
36 |
35 |
37 fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *) |
36 fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *) |
38 fun reduce_to_non_proper_sort (TVar (name, sort)) = |
37 fun reduce_to_non_proper_sort (TVar (name, sort)) = |
39 TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort))) |
38 TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort))) |
40 | reduce_to_non_proper_sort _ = error "not supported"; |
39 | reduce_to_non_proper_sort _ = error "not supported"; |
41 |
40 |
42 val data = (map fst classes) ~~ assms; |
41 val data = map #1 (#outer_constraints ucontext) ~~ #constraints ucontext; |
43 |
42 |
44 val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar' |
43 val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar' |
45 then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data |
44 then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data |
46 |> the_default tvar; |
45 |> the_default tvar; |
47 |
46 |