src/CTT/CTT.thy

 subsection \<open>Tactics for type checking\<close>
 
 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
 
 (*Try solving a:A or a=b:A by assumption provided a is rigid!*)