src/CCL/Wfd.thy
changeset 74375 ba880f3a4e52
parent 74298 45a77ee63e57
child 74563 042041c0ebeb
--- a/src/CCL/Wfd.thy	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/CCL/Wfd.thy	Tue Sep 28 17:09:05 2021 +0200
@@ -441,7 +441,7 @@
 
 fun is_rigid_prog t =
   (case (Logic.strip_assums_concl t) of
-    \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem _ for a _\<close>\<close>\<close> => null (Term.add_vars a [])
+    \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem _ for a _\<close>\<close> => null (Term.add_vars a [])
   | _ => false)
 
 in