adapted typed_print_translation;
authorwenzelm
Wed Nov 05 11:49:34 1997 +0100 (1997-11-05)
changeset 41515c19cd418c33
parent 4150 56025371fc02
child 4152 451104c223e2
adapted typed_print_translation;
src/HOL/List.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/List.thy	Wed Nov 05 11:49:07 1997 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Nov 05 11:49:34 1997 +0100
     1.3 @@ -132,9 +132,9 @@
     1.4  
     1.5  (* translating size::list -> length *)
     1.6  
     1.7 -fun size_tr' (Type ("fun", (Type ("list", _) :: _))) [t] =
     1.8 +fun size_tr' _ (Type ("fun", (Type ("list", _) :: _))) [t] =
     1.9        Syntax.const "length" $ t
    1.10 -  | size_tr'   _ _ = raise Match;
    1.11 +  | size_tr' _ _ _ = raise Match;
    1.12  
    1.13  in
    1.14  
     2.1 --- a/src/HOL/Set.thy	Wed Nov 05 11:49:07 1997 +0100
     2.2 +++ b/src/HOL/Set.thy	Wed Nov 05 11:49:34 1997 +0100
     2.3 @@ -163,13 +163,13 @@
     2.4  
     2.5  (* Set inclusion *)
     2.6  
     2.7 -fun le_tr' (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
     2.8 +fun le_tr' _ (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
     2.9        list_comb (Syntax.const "_setle", ts)
    2.10 -  | le_tr' (*op <=*) _ _ = raise Match;
    2.11 +  | le_tr' _ (*op <=*) _ _ = raise Match;
    2.12  
    2.13 -fun less_tr' (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
    2.14 +fun less_tr' _ (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
    2.15        list_comb (Syntax.const "_setless", ts)
    2.16 -  | less_tr' (*op <*) _ _ = raise Match;
    2.17 +  | less_tr' _ (*op <*) _ _ = raise Match;
    2.18  
    2.19  
    2.20  (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)