equal
deleted
inserted
replaced
500 shyps = |
500 shyps = |
501 (if eq_set_sort (shyps',sorts) orelse |
501 (if eq_set_sort (shyps',sorts) orelse |
502 not (!force_strip_shyps) then shyps' |
502 not (!force_strip_shyps) then shyps' |
503 else (* FIXME tmp *) |
503 else (* FIXME tmp *) |
504 (warning ("Removed sort hypotheses: " ^ |
504 (warning ("Removed sort hypotheses: " ^ |
505 commas (map Type.str_of_sort (shyps' \\ sorts))); |
505 commas (map Sorts.str_of_sort (shyps' \\ sorts))); |
506 warning "Let's hope these sorts are non-empty!"; |
506 warning "Let's hope these sorts are non-empty!"; |
507 sorts)), |
507 sorts)), |
508 hyps = hyps, |
508 hyps = hyps, |
509 prop = prop} |
509 prop = prop} |
510 end; |
510 end; |