--- a/src/CTT/CTT.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/CTT/CTT.thy Fri Jan 04 23:22:53 2019 +0100
@@ -304,9 +304,9 @@
ML \<open>
local
-fun is_rigid_elem (Const(@{const_name Elem},_) $ a $ _) = not(is_Var (head_of a))
- | is_rigid_elem (Const(@{const_name Eqelem},_) $ a $ _ $ _) = not(is_Var (head_of a))
- | is_rigid_elem (Const(@{const_name Type},_) $ a) = not(is_Var (head_of a))
+fun is_rigid_elem (Const(\<^const_name>\<open>Elem\<close>,_) $ a $ _) = not(is_Var (head_of a))
+ | is_rigid_elem (Const(\<^const_name>\<open>Eqelem\<close>,_) $ a $ _ $ _) = not(is_Var (head_of a))
+ | is_rigid_elem (Const(\<^const_name>\<open>Type\<close>,_) $ a) = not(is_Var (head_of a))
| is_rigid_elem _ = false
in