src/ZF/intr_elim.ML

 
 val dummy = assert_all (is_some o lookup_const sign) rec_names
    (fn a => "Name of recursive set not declared as constant: " ^ a);
 
 val intr_tms = map (Sign.term_of o rd propT) sintrs;
-val (Const(_,recT),rec_params) = strip_comb (#2 (rule_concl(hd intr_tms)))
+
+local (*Checking the introduction rules*)
+  val intr_sets = map (#2 o rule_concl) 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
+     (fn t => "Conclusion of rule does not name a recursive set: " ^ 
+	      Sign.string_of_term sign t);
+in
+val (Const(_,recT),rec_params) = strip_comb (hd intr_sets)
+end;
+
 val rec_hds = map (fn a=> Const(a,recT)) rec_names;
 val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
 
 val dummy = assert_all is_Free rec_params
     (fn t => "Param in recursion term not a free variable: " ^

               ORELSE' bound_hyp_subst_tac))
     THEN prune_params_tac;
 
 val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
 
-(*Applies freeness of the given constructors.
-  NB for datatypes, defs=con_defs; for inference systems, con_defs=[]! *)
+(*Applies freeness of the given constructors, which *must* be unfolded by
+  the given defs.  Cannot simply use the local con_defs because con_defs=[] 
+  for inference systems. *)
 fun con_elim_tac defs =
     rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
 
 (*String s should have the form t:Si where Si is an inductive set*)
 fun mk_cases defs s =