diff -r 47be9d22a0d6 -r 4a2bb4fbc168 intr_elim.ML
--- a/intr_elim.ML	Wed Aug 31 16:25:19 1994 +0200
+++ b/intr_elim.ML	Wed Aug 31 17:50:59 1994 +0200
@@ -113,9 +113,19 @@
 
 (*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 =