src/HOL/Transitive_Closure.thy

   val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
   val rtrancl_trans = @{thm rtrancl_trans};
 
   fun decomp (@{const Trueprop} $ t) =
     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+")
+        let fun decr (Const (@{const_name rtrancl}, _ ) $ r) = (r,"r*")
+              | decr (Const (@{const_name trancl}, _ ) $ r)  = (r,"r+")
               | decr r = (r,"r");
             val (rel,r) = decr (Envir.beta_eta_contract rel);
         in SOME (a,b,rel,r) end
       | dec _ =  NONE
     in dec t end

   val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
   val rtrancl_trans = @{thm rtranclp_trans};
 
   fun decomp (@{const Trueprop} $ t) =
     let fun dec (rel $ a $ b) =
-        let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $ r) = (r,"r*")
-              | decr (Const ("Transitive_Closure.tranclp", _ ) $ r)  = (r,"r+")
+        let fun decr (Const (@{const_name rtranclp}, _ ) $ r) = (r,"r*")
+              | decr (Const (@{const_name tranclp}, _ ) $ r)  = (r,"r+")
               | decr r = (r,"r");
             val (rel,r) = decr rel;
         in SOME (a, b, rel, r) end
       | dec _ =  NONE
     in dec t end