# HG changeset patch
# User berghofe
# Date 1210150609 -7200
# Node ID 244184661a097b3f40cb1be90b79b56b5747d4a8
# Parent  dcf1dfc915a701611ce9b55d41fa6a41e5750f5f
- 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.

diff -r dcf1dfc915a7 -r 244184661a09 src/HOL/Transitive_Closure.thy
--- 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;