# HG changeset patch
# User wenzelm
# Date 1631470176 -7200
# Node ID 45a77ee63e575f7261386d93dda40769ff918251
# Parent  ac130a6bd6b2db6158c5fb238ac39e94f6f5df8b
more antiquotations;

diff -r ac130a6bd6b2 -r 45a77ee63e57 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Sat Sep 11 22:38:41 2021 +0200
+++ b/src/CCL/Wfd.thy	Sun Sep 12 20:09:36 2021 +0200
@@ -413,13 +413,13 @@
   @{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
   @{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
 
-fun bvars (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(s,_,t)) l = bvars t (s::l)
+fun bvars \<^Const_>\<open>Pure.all _ for \<open>Abs(s,_,t)\<close>\<close> l = bvars t (s::l)
   | bvars _ l = l
 
-fun get_bno l n (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(s,_,t)) = get_bno (s::l) n t
-  | get_bno l n (Const(\<^const_name>\<open>Trueprop\<close>,_) $ t) = get_bno l n t
-  | get_bno l n (Const(\<^const_name>\<open>Ball\<close>,_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
-  | get_bno l n (Const(\<^const_name>\<open>mem\<close>,_) $ t $ _) = get_bno l n t
+fun get_bno l n \<^Const_>\<open>Pure.all _ for \<open>Abs(s,_,t)\<close>\<close> = get_bno (s::l) n t
+  | get_bno l n \<^Const_>\<open>Trueprop for t\<close> = get_bno l n t
+  | get_bno l n \<^Const_>\<open>Ball _ for _ \<open>Abs(s,_,t)\<close>\<close> = get_bno (s::l) (n+1) t
+  | get_bno l n \<^Const_>\<open>mem _ for t _\<close> = get_bno l n t
   | get_bno l n (t $ s) = get_bno l n t
   | get_bno l n (Bound m) = (m-length(l),n)
 
@@ -441,8 +441,7 @@
 
 fun is_rigid_prog t =
   (case (Logic.strip_assums_concl t) of
-    (Const(\<^const_name>\<open>Trueprop\<close>,_) $ (Const(\<^const_name>\<open>mem\<close>,_) $ a $ _)) =>
-      null (Term.add_vars a [])
+    \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem _ for a _\<close>\<close>\<close> => null (Term.add_vars a [])
   | _ => false)
 
 in