src/CCL/Wfd.thy
changeset 38500 d5477ee35820
parent 36319 8feb2c4bef1a
child 41526 54b4686704af
--- a/src/CCL/Wfd.thy	Tue Aug 17 19:36:38 2010 +0200
+++ b/src/CCL/Wfd.thy	Tue Aug 17 19:36:39 2010 +0200
@@ -423,13 +423,13 @@
   @{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
   @{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
 
-fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l)
+fun bvars (Const(@{const_name all},_) $ Abs(s,_,t)) l = bvars t (s::l)
   | bvars _ l = l
 
-fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t
-  | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t
-  | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
-  | get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t
+fun get_bno l n (Const(@{const_name all},_) $ Abs(s,_,t)) = get_bno (s::l) n t
+  | get_bno l n (Const(@{const_name Trueprop},_) $ t) = get_bno l n t
+  | get_bno l n (Const(@{const_name Ball},_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
+  | get_bno l n (Const(@{const_name mem},_) $ t $ _) = 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)
 
@@ -450,7 +450,7 @@
 
 fun is_rigid_prog t =
      case (Logic.strip_assums_concl t) of
-        (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => null (Term.add_vars a [])
+        (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) => null (Term.add_vars a [])
        | _ => false
 in