Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/List.thy
changeset 4151 5c19cd418c33
parent 4132 daff3c9987cc
child 4502 337c073de95e 
--- 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
isabelle