src/HOL/Set.thy
changeset 4151 5c19cd418c33
parent 3947 eb707467f8c5
child 4159 4aff9b7e5597
     1.1 --- a/src/HOL/Set.thy	Wed Nov 05 11:49:07 1997 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Nov 05 11:49:34 1997 +0100
     1.3 @@ -163,13 +163,13 @@
     1.4  
     1.5  (* Set inclusion *)
     1.6  
     1.7 -fun le_tr' (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
     1.8 +fun le_tr' _ (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
     1.9        list_comb (Syntax.const "_setle", ts)
    1.10 -  | le_tr' (*op <=*) _ _ = raise Match;
    1.11 +  | le_tr' _ (*op <=*) _ _ = raise Match;
    1.12  
    1.13 -fun less_tr' (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
    1.14 +fun less_tr' _ (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
    1.15        list_comb (Syntax.const "_setless", ts)
    1.16 -  | less_tr' (*op <*) _ _ = raise Match;
    1.17 +  | less_tr' _ (*op <*) _ _ = raise Match;
    1.18  
    1.19  
    1.20  (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)