- Function dec in Trancl_Tac must eta-contract relation before calling
decr, since it is now a function and could therefore be in eta-expanded form
- The trancl prover now does more eta-contraction itself, so eta-contraction
is no longer necessary in Tranclp_tac.

--- a/src/HOL/Transitive_Closure.thy	Wed May 07 10:56:43 2008 +0200
+++ b/src/HOL/Transitive_Closure.thy	Wed May 07 10:56:49 2008 +0200
@@ -636,7 +636,7 @@
         let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
               | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
               | decr r = (r,"r");
-            val (rel,r) = decr rel;
+            val (rel,r) = decr (Envir.beta_eta_contract rel);
         in SOME (a,b,rel,r) end
       | dec _ =  NONE
     in dec t end;
@@ -660,7 +660,7 @@
               | decr (Const ("Transitive_Closure.tranclp", _ ) $ r)  = (r,"r+")
               | decr r = (r,"r");
             val (rel,r) = decr rel;
-        in SOME (a, b, Envir.beta_eta_contract rel, r) end
+        in SOME (a, b, rel, r) end
       | dec _ =  NONE
     in dec t end;