--- a/indrule.ML Fri Nov 25 14:39:13 1994 +0100
+++ b/indrule.ML Fri Nov 25 16:24:18 1994 +0100
@@ -25,7 +25,7 @@
val (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
-val elem_type = dest_set (body_type recT);
+val elem_type = dest_setT (body_type recT);
val domTs = summands(elem_type);
val big_rec_name = space_implode "_" rec_names;
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
@@ -44,7 +44,7 @@
fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $
(Const("op :",_)$t$X), iprems) =
(case gen_assoc (op aconv) (ind_alist, X) of
- Some pred => prem :: mk_tprop (pred $ t) :: iprems
+ Some pred => prem :: mk_Trueprop (pred $ t) :: iprems
| None => (*possibly membership in M(rec_tm), for M monotone*)
let fun mk_sb (rec_tm,pred) =
(case binder_types (fastype_of pred) of
@@ -62,7 +62,7 @@
(strip_imp_prems intr,[])
val (t,X) = rule_concl intr
val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
- val concl = mk_tprop (pred $ t)
+ val concl = mk_Trueprop (pred $ t)
in list_all_free (quantfrees, list_implies (iprems,concl)) end
handle Bind => error"Recursion term not found in conclusion";
@@ -79,7 +79,7 @@
val quant_induct =
prove_goalw_cterm part_rec_defs
(cterm_of sign (list_implies (ind_prems,
- mk_tprop (mk_all_imp(big_rec_tm,pred)))))
+ mk_Trueprop (mk_all_imp(big_rec_tm,pred)))))
(fn prems =>
[rtac (impI RS allI) 1,
etac raw_induct 1,
@@ -117,11 +117,11 @@
(*To instantiate the main induction rule*)
val induct_concl =
- mk_tprop(mk_all_imp(big_rec_tm,
+ mk_Trueprop(mk_all_imp(big_rec_tm,
Abs("z", elem_type,
fold_bal (app conj)
(map mk_rec_imp (rec_tms~~preds)))))
-and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);
+and mutual_induct_concl = mk_Trueprop(fold_bal (app conj) qconcls);
val lemma = (*makes the link between the two induction rules*)
prove_goalw_cterm part_rec_defs