src/HOL/Transitive_Closure.thy
changeset 37391 476270a6c2dc
parent 35216 7641e8d831d2
child 37677 c5a8b612e571
     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Jun 10 12:24:02 2010 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Jun 10 12:24:03 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 ("Pair", _) $ a $ b) $ rel ) =
     1.8 +    let fun dec (Const ("op :", _) $ (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");