# HG changeset patch
# User paulson
# Date 857986352 -3600
# Node ID 9c42ae57b5f4840ba9ba1f012c7b0a7e9c29f73d
# Parent  40219658ce6461192b3eb91bb3838ef6776b468c
The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac
does not recognize eta-equality.  But making it do so is costly

diff -r 40219658ce64 -r 9c42ae57b5f4 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Mar 07 16:44:28 1997 +0100
+++ b/src/HOL/MiniML/W.ML	Mon Mar 10 10:32:32 1997 +0100
@@ -513,9 +513,10 @@
 by (rotate_tac ~3 1);
 by (Asm_full_simp_tac 1);
 by (safe_tac HOL_cs);
+by (contr_tac 1);
 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
         conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1);
-
+(** LEVEL 35 **)
 by (subgoal_tac
   "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
 \        else Ra x)) ($ Sa t) = \