# HG changeset patch
# User lcp
# Date 806684485 -7200
# Node ID d7e0c280f261c0e0a14f406b07f5659b048d5da9
# Parent  9d1bdce3a38e86b7e5e62490fb39ed2b8d945a36
Added two final lines to intro_tacsf for mutual recursion
(borrowed from ZF version)

diff -r 9d1bdce3a38e -r d7e0c280f261 src/HOL/intr_elim.ML
--- a/src/HOL/intr_elim.ML	Tue Jul 25 17:00:53 1995 +0200
+++ b/src/HOL/intr_elim.ML	Tue Jul 25 17:01:25 1995 +0200
@@ -85,7 +85,11 @@
    rtac disjIn 1,
    (*Not ares_tac, since refl must be tried before any equality assumptions;
      backtracking may occur if the premises have extra variables!*)
-   DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 ORELSE assume_tac 1)];
+   DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 ORELSE assume_tac 1),
+   (*Now solve the equations like Inl 0 = Inl ?b2*)
+   rewrite_goals_tac con_defs,
+   REPEAT (rtac refl 1)];
+
 
 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
 val mk_disj_rls =