761 let val dummy = say "restrict_prover:" |
761 let val dummy = say "restrict_prover:" |
762 val cntxt = rev(MetaSimplifier.prems_of_ss ss) |
762 val cntxt = rev(MetaSimplifier.prems_of_ss ss) |
763 val dummy = print_thms "cntxt:" cntxt |
763 val dummy = print_thms "cntxt:" cntxt |
764 val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _, |
764 val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _, |
765 sign,...} = rep_thm thm |
765 sign,...} = rep_thm thm |
766 fun genl tm = let val vlist = gen_rems (op aconv) |
766 fun genl tm = let val vlist = subtract (op aconv) globals |
767 (add_term_frees(tm,[]), globals) |
767 (add_term_frees(tm,[])) |
768 in fold_rev Forall vlist tm |
768 in fold_rev Forall vlist tm |
769 end |
769 end |
770 (*-------------------------------------------------------------- |
770 (*-------------------------------------------------------------- |
771 * This actually isn't quite right, since it will think that |
771 * This actually isn't quite right, since it will think that |
772 * not-fully applied occs. of "f" in the context mean that the |
772 * not-fully applied occs. of "f" in the context mean that the |