src/ZF/intr_elim.ML

    (fn a => "Name of recursive set not declared as constant: " ^ a);
 
 val intr_tms = map (term_of o rd propT) sintrs;
 
 local (*Checking the introduction rules*)
-  val intr_sets = map (#2 o rule_concl) intr_tms;
+  val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
 
   fun intr_ok set =
       case head_of set of Const(a,recT) => a mem rec_names | _ => false;
 
   val dummy =  assert_all intr_ok intr_sets

   | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
 	deny (rec_hd occs t) "Recursion term on left of member symbol"
   | chk_prem rec_hd t = 
 	deny (rec_hd occs t) "Recursion term in side formula";
 
+fun dest_tprop (Const("Trueprop",_) $ P) = P
+  | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
+			  Sign.string_of_term sign Q);
+
 (*Makes a disjunct from an introduction rule*)
 fun lfp_part intr = (*quantify over rule's free vars except parameters*)
   let val prems = map dest_tprop (strip_imp_prems intr)
       val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
       val exfrees = term_frees intr \\ rec_params

 val big_rec_def::part_rec_defs = defs;
 
 val prove = prove_term (sign_of thy);
 
 (********)
-val dummy = writeln "Proving monotonocity...";
+val dummy = writeln "Proving monotonicity...";
 
 val bnd_mono = 
     prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs), 
        fn _ =>
        [rtac (Collect_subset RS bnd_monoI) 1,