diff -r 6be2f3e03786 -r fcf8024c920d indrule.ML
--- 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