equal
deleted
inserted
replaced
1055 |
1055 |
1056 in |
1056 in |
1057 |
1057 |
1058 fun of_sort_proof thy hyps = |
1058 fun of_sort_proof thy hyps = |
1059 Sorts.of_sort_derivation (Sign.classes_of thy) |
1059 Sorts.of_sort_derivation (Sign.classes_of thy) |
1060 {class_relation = fn typ => fn (prf, c1) => fn c2 => |
1060 {class_relation = fn typ => fn _ => fn (prf, c1) => fn c2 => |
1061 if c1 = c2 then prf |
1061 if c1 = c2 then prf |
1062 else canonical_instance [typ] (classrel_proof thy (c1, c2)) %% prf, |
1062 else canonical_instance [typ] (classrel_proof thy (c1, c2)) %% prf, |
1063 type_constructor = fn (a, typs) => fn dom => fn c => |
1063 type_constructor = fn (a, typs) => fn dom => fn c => |
1064 let val Ss = map (map snd) dom and prfs = maps (map fst) dom |
1064 let val Ss = map (map snd) dom and prfs = maps (map fst) dom |
1065 in proof_combP (canonical_instance typs (arity_proof thy (a, Ss, c)), prfs) end, |
1065 in proof_combP (canonical_instance typs (arity_proof thy (a, Ss, c)), prfs) end, |