463 (*** Meta rules ***) |
463 (*** Meta rules ***) |
464 |
464 |
465 (** sort contexts **) |
465 (** sort contexts **) |
466 |
466 |
467 (*account for lost sort constraints*) |
467 (*account for lost sort constraints*) |
468 fun fix_shyps ths Ts th = |
468 fun fix_shyps ths Ts th = th; |
|
469 (* FIXME |
469 let |
470 let |
470 fun thm_sorts (Thm {shyps, hyps, prop, ...}) = |
471 fun thm_sorts (Thm {shyps, hyps, prop, ...}) = |
471 unions (shyps :: term_sorts prop :: map term_sorts hyps); |
472 unions (shyps :: term_sorts prop :: map term_sorts hyps); |
472 val lost_sorts = |
473 val lost_sorts = |
473 unions (map thm_sorts ths @ map typ_sorts Ts) \\ thm_sorts th; |
474 unions (map thm_sorts ths @ map typ_sorts Ts) \\ thm_sorts th; |
474 val Thm {sign, maxidx, shyps, hyps, prop} = th; |
475 val Thm {sign, maxidx, shyps, hyps, prop} = th; |
475 in |
476 in |
476 Thm {sign = sign, maxidx = maxidx, |
477 Thm {sign = sign, maxidx = maxidx, |
477 shyps = lost_sorts @ shyps, hyps = hyps, prop = prop} |
478 shyps = lost_sorts @ shyps, hyps = hyps, prop = prop} |
478 end; |
479 end; |
479 |
480 *) |
480 (*remove sorts that are known to be non-empty (syntactically)*) |
481 (*remove sorts that are known to be non-empty (syntactically)*) |
481 val force_strip_shyps = ref true; (* FIXME tmp *) |
482 val force_strip_shyps = ref true; (* FIXME tmp *) |
482 fun strip_shyps th = |
483 fun strip_shyps th = |
483 let |
484 let |
484 fun sort_hyps_of t = |
485 fun sort_hyps_of t = |