- Function dec in Trancl_Tac must eta-contract relation before calling
authorberghofe
Wed May 07 10:56:49 2008 +0200 (2008-05-07)
changeset 26801244184661a09
parent 26800 dcf1dfc915a7
child 26802 9eede540a5e8
- 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.
src/HOL/Transitive_Closure.thy
     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