--- a/src/HOL/Transitive_Closure.thy Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Jul 01 16:54:42 2010 +0200
@@ -858,7 +858,7 @@
val rtrancl_trans = @{thm rtrancl_trans};
fun decomp (@{const Trueprop} $ t) =
- let fun dec (Const ("op :", _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
+ let fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
| decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+")
| decr r = (r,"r");