--- a/src/HOL/Transitive_Closure.thy Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Transitive_Closure.thy Tue Sep 28 17:09:05 2021 +0200
@@ -1289,7 +1289,7 @@
fun decomp \<^Const_>\<open>Trueprop for t\<close> =
let
- fun dec \<^Const_>\<open>Set.member _ for \<open>\<^Const_>\<open>Pair _ _ for a b\<close>\<close> rel\<close> =
+ fun dec \<^Const_>\<open>Set.member _ for \<^Const_>\<open>Pair _ _ for a b\<close> rel\<close> =
let
fun decr \<^Const_>\<open>rtrancl _ for r\<close> = (r,"r*")
| decr \<^Const_>\<open>trancl _ for r\<close> = (r,"r+")