Fixed print translation for ALL x > y etc
authornipkow
Thu Dec 02 12:28:09 2004 +0100 (2004-12-02)
changeset 15363885a40edcdba
parent 15362 a000b267be57
child 15364 0c3891c3528f
Fixed print translation for ALL x > y etc
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Thu Dec 02 11:59:34 2004 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Dec 02 12:28:09 2004 +0100
     1.3 @@ -1154,38 +1154,40 @@
     1.4  
     1.5  print_translation {*
     1.6  let
     1.7 +  fun mk v v' q n P =
     1.8 +    if v=v' andalso not(v  mem (map fst (Term.add_frees([],n))))
     1.9 +    then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
    1.10    fun all_tr' [Const ("_bound",_) $ Free (v,_), 
    1.11                 Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.12 -  (if v=v' then Syntax.const "_lessAll" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.13 +    mk v v' "_lessAll" n P
    1.14  
    1.15    | all_tr' [Const ("_bound",_) $ Free (v,_), 
    1.16                 Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.17 -  (if v=v' then Syntax.const "_leAll" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.18 +    mk v v' "_leAll" n P
    1.19  
    1.20    | all_tr' [Const ("_bound",_) $ Free (v,_), 
    1.21                 Const("op -->",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
    1.22 -  (if v=v' then Syntax.const "_gtAll" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.23 +    mk v v' "_gtAll" n P
    1.24  
    1.25    | all_tr' [Const ("_bound",_) $ Free (v,_), 
    1.26                 Const("op -->",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
    1.27 -  (if v=v' then Syntax.const "_geAll" $ Syntax.mark_bound v' $ n $ P else raise Match);
    1.28 +    mk v v' "_geAll" n P;
    1.29  
    1.30    fun ex_tr' [Const ("_bound",_) $ Free (v,_), 
    1.31                 Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.32 -  (if v=v' then Syntax.const "_lessEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.33 +    mk v v' "_lessEx" n P
    1.34  
    1.35    | ex_tr' [Const ("_bound",_) $ Free (v,_), 
    1.36                 Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.37 -  (if v=v' then Syntax.const "_leEx" $ Syntax.mark_bound v' $ n $ P else
    1.38 -               raise Match)
    1.39 +    mk v v' "_leEx" n P
    1.40  
    1.41    | ex_tr' [Const ("_bound",_) $ Free (v,_), 
    1.42                 Const("op &",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
    1.43 -  (if v=v' then Syntax.const "_gtEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.44 +    mk v v' "_gtEx" n P
    1.45  
    1.46    | ex_tr' [Const ("_bound",_) $ Free (v,_), 
    1.47                 Const("op &",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
    1.48 -  (if v=v' then Syntax.const "_geEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.49 +    mk v v' "_geEx" n P
    1.50  in
    1.51  [("ALL ", all_tr'), ("EX ", ex_tr')]
    1.52  end