Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/CTT/CTT.thy
changeset 56250 2c9f841f36b8
parent 51308 51e158e988a5
child 58889 5b7a9633cfa8 
--- a/src/CTT/CTT.thy	Sat Mar 22 15:58:27 2014 +0100
+++ b/src/CTT/CTT.thy	Sat Mar 22 16:50:52 2014 +0100
@@ -328,9 +328,9 @@
 
 local
 
-fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
-  | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
-  | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
+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))
   | is_rigid_elem _ = false
 
 in
isabelle