src/HOL/Transitive_Closure.thy
changeset 37677 c5a8b612e571
parent 37391 476270a6c2dc
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Jul 01 16:54:42 2010 +0200
     1.3 @@ -858,7 +858,7 @@
     1.4    val rtrancl_trans = @{thm rtrancl_trans};
     1.5  
     1.6    fun decomp (@{const Trueprop} $ t) =
     1.7 -    let fun dec (Const ("op :", _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
     1.8 +    let fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
     1.9          let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
    1.10                | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
    1.11                | decr r = (r,"r");