intr_elim.ML

 
 val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
 
 (*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. *)
+  for inference systems.
 fun con_elim_tac defs =
     rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
+ *)
+fun con_elim_tac simps =
+  let val elim_tac = REPEAT o (eresolve_tac (elim_rls@sumprod_free_SEs))
+  in ALLGOALS(EVERY'[elim_tac,
+                     asm_full_simp_tac (nat_ss addsimps simps),
+                     elim_tac,
+                     REPEAT o bound_hyp_subst_tac])
+     THEN prune_params_tac
+  end;
+
 
 (*String s should have the form t:Si where Si is an inductive set*)
 fun mk_cases defs s = 
     rule_by_tactic (con_elim_tac defs)
       (assume_read thy s  RS  elim);