equal
deleted
inserted
replaced
1062 |
1062 |
1063 (** type classes **) |
1063 (** type classes **) |
1064 |
1064 |
1065 fun strip_shyps_proof algebra present witnessed extra_sorts prf = |
1065 fun strip_shyps_proof algebra present witnessed extra_sorts prf = |
1066 let |
1066 let |
1067 fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE; |
1067 fun get S (T', S') = if Sorts.sort_le algebra (S', S) then SOME T' else NONE; |
1068 val extra = map (`Logic.dummy_tfree) extra_sorts; |
1068 val extra = map (`Logic.dummy_tfree) extra_sorts; |
1069 val replacements = present @ extra @ witnessed; |
1069 val replacements = present @ extra @ witnessed; |
1070 fun replace T = |
1070 fun replace T = |
1071 if exists (fn (T', _) => T' = T) present then raise Same.SAME |
1071 if exists (fn (T', _) => T' = T) present then raise Same.SAME |
1072 else |
1072 else |