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