--- 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 =