equal
deleted
inserted
replaced
1023 I) |
1023 I) |
1024 and add_axioms_for_sort depth T S = |
1024 and add_axioms_for_sort depth T S = |
1025 let |
1025 let |
1026 val supers = Sign.complete_sort thy S |
1026 val supers = Sign.complete_sort thy S |
1027 val class_axioms = |
1027 val class_axioms = |
1028 maps (fn class => map prop_of (Axclass.get_info thy class |> #axioms |
1028 maps (fn class => map Thm.prop_of (Axclass.get_info thy class |> #axioms |
1029 handle ERROR _ => [])) supers |
1029 handle ERROR _ => [])) supers |
1030 val monomorphic_class_axioms = |
1030 val monomorphic_class_axioms = |
1031 map (fn t => case Term.add_tvars t [] of |
1031 map (fn t => case Term.add_tvars t [] of |
1032 [] => t |
1032 [] => t |
1033 | [(x, S)] => |
1033 | [(x, S)] => |