equal
deleted
inserted
replaced
889 (**** sort hypotheses ****) |
889 (**** sort hypotheses ****) |
890 |
890 |
891 fun strip_shyps_proof algebra present witnessed extra_sorts prf = |
891 fun strip_shyps_proof algebra present witnessed extra_sorts prf = |
892 let |
892 let |
893 fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE; |
893 fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE; |
894 val extra = map (fn S => (TFree (Name.aT, S), S)) extra_sorts; |
894 val extra = map (fn S => (TFree ("'dummy", S), S)) extra_sorts; |
895 val replacements = present @ extra @ witnessed; |
895 val replacements = present @ extra @ witnessed; |
896 fun replace T = |
896 fun replace T = |
897 if exists (fn (T', _) => T' = T) present then raise Same.SAME |
897 if exists (fn (T', _) => T' = T) present then raise Same.SAME |
898 else |
898 else |
899 (case get_first (get (Type.sort_of_atyp T)) replacements of |
899 (case get_first (get (Type.sort_of_atyp T)) replacements of |