src/HOL/Transitive_Closure.thy
changeset 26801 244184661a09
parent 26340 a85fe32e7b2f
child 29609 a010aab5bed0
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed May 07 10:56:43 2008 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed May 07 10:56:49 2008 +0200
     1.3 @@ -636,7 +636,7 @@
     1.4          let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
     1.5                | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
     1.6                | decr r = (r,"r");
     1.7 -            val (rel,r) = decr rel;
     1.8 +            val (rel,r) = decr (Envir.beta_eta_contract rel);
     1.9          in SOME (a,b,rel,r) end
    1.10        | dec _ =  NONE
    1.11      in dec t end;
    1.12 @@ -660,7 +660,7 @@
    1.13                | decr (Const ("Transitive_Closure.tranclp", _ ) $ r)  = (r,"r+")
    1.14                | decr r = (r,"r");
    1.15              val (rel,r) = decr rel;
    1.16 -        in SOME (a, b, Envir.beta_eta_contract rel, r) end
    1.17 +        in SOME (a, b, rel, r) end
    1.18        | dec _ =  NONE
    1.19      in dec t end;
    1.20