--- a/src/HOL/List.thy Wed Nov 05 11:49:07 1997 +0100
+++ b/src/HOL/List.thy Wed Nov 05 11:49:34 1997 +0100
@@ -132,9 +132,9 @@
(* translating size::list -> length *)
-fun size_tr' (Type ("fun", (Type ("list", _) :: _))) [t] =
+fun size_tr' _ (Type ("fun", (Type ("list", _) :: _))) [t] =
Syntax.const "length" $ t
- | size_tr' _ _ = raise Match;
+ | size_tr' _ _ _ = raise Match;
in
--- a/src/HOL/Set.thy Wed Nov 05 11:49:07 1997 +0100
+++ b/src/HOL/Set.thy Wed Nov 05 11:49:34 1997 +0100
@@ -163,13 +163,13 @@
(* Set inclusion *)
-fun le_tr' (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
+fun le_tr' _ (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
list_comb (Syntax.const "_setle", ts)
- | le_tr' (*op <=*) _ _ = raise Match;
+ | le_tr' _ (*op <=*) _ _ = raise Match;
-fun less_tr' (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
+fun less_tr' _ (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
list_comb (Syntax.const "_setless", ts)
- | less_tr' (*op <*) _ _ = raise Match;
+ | less_tr' _ (*op <*) _ _ = raise Match;
(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *)