src/CCL/Wfd.thy
changeset 56245 84fc7dfa3cd4
parent 51798 ad3a241def73
child 57521 b14c0794f97f
     1.1 --- a/src/CCL/Wfd.thy	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/CCL/Wfd.thy	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -423,10 +423,10 @@
     1.4    @{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
     1.5    @{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
     1.6  
     1.7 -fun bvars (Const(@{const_name all},_) $ Abs(s,_,t)) l = bvars t (s::l)
     1.8 +fun bvars (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) l = bvars t (s::l)
     1.9    | bvars _ l = l
    1.10  
    1.11 -fun get_bno l n (Const(@{const_name all},_) $ Abs(s,_,t)) = get_bno (s::l) n t
    1.12 +fun get_bno l n (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) = get_bno (s::l) n t
    1.13    | get_bno l n (Const(@{const_name Trueprop},_) $ t) = get_bno l n t
    1.14    | get_bno l n (Const(@{const_name Ball},_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
    1.15    | get_bno l n (Const(@{const_name mem},_) $ t $ _) = get_bno l n t