src/HOL/Transitive_Closure.thy
changeset 30107 f3b3b0e3d184
parent 29609 a010aab5bed0
child 30198 922f944f03b2
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Feb 25 11:30:46 2009 -0800
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Feb 26 16:32:46 2009 +0100
     1.3 @@ -646,7 +646,7 @@
     1.4      val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
     1.5      val rtrancl_trans = @{thm rtrancl_trans};
     1.6  
     1.7 -  fun decomp (Trueprop $ t) =
     1.8 +  fun decomp (@{const Trueprop} $ t) =
     1.9      let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
    1.10          let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
    1.11                | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
    1.12 @@ -654,7 +654,8 @@
    1.13              val (rel,r) = decr (Envir.beta_eta_contract rel);
    1.14          in SOME (a,b,rel,r) end
    1.15        | dec _ =  NONE
    1.16 -    in dec t end;
    1.17 +    in dec t end
    1.18 +    | decomp _ = NONE;
    1.19  
    1.20    end);
    1.21  
    1.22 @@ -669,7 +670,7 @@
    1.23      val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
    1.24      val rtrancl_trans = @{thm rtranclp_trans};
    1.25  
    1.26 -  fun decomp (Trueprop $ t) =
    1.27 +  fun decomp (@{const Trueprop} $ t) =
    1.28      let fun dec (rel $ a $ b) =
    1.29          let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $ r) = (r,"r*")
    1.30                | decr (Const ("Transitive_Closure.tranclp", _ ) $ r)  = (r,"r+")
    1.31 @@ -677,7 +678,8 @@
    1.32              val (rel,r) = decr rel;
    1.33          in SOME (a, b, rel, r) end
    1.34        | dec _ =  NONE
    1.35 -    in dec t end;
    1.36 +    in dec t end
    1.37 +    | decomp _ = NONE;
    1.38  
    1.39    end);
    1.40  *}