# HG changeset patch
# User wenzelm
# Date 1631470280 -7200
# Node ID 16e5870fe21eb6f7e87646fd1571c4a2209583ac
# Parent  45a77ee63e575f7261386d93dda40769ff918251
more antiquotations;

diff -r 45a77ee63e57 -r 16e5870fe21e src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Sun Sep 12 20:09:36 2021 +0200
+++ b/src/CTT/CTT.thy	Sun Sep 12 20:11:20 2021 +0200
@@ -304,9 +304,9 @@
 ML \<open>
 local
 
-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))
+fun is_rigid_elem \<^Const_>\<open>Elem for a _\<close> = not(is_Var (head_of a))
+  | is_rigid_elem \<^Const_>\<open>Eqelem for a _ _\<close> = not(is_Var (head_of a))
+  | is_rigid_elem \<^Const_>\<open>Type for a\<close> = not(is_Var (head_of a))
   | is_rigid_elem _ = false
 
 in