--- a/src/ZF/listfn.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/listfn.thy Tue Nov 16 14:24:21 1993 +0100
@@ -10,7 +10,7 @@
although complicating its derivation.
*)
-ListFn = List +
+ListFn = List + "constructor" +
consts
"@" :: "[i,i]=>i" (infixr 60)
list_rec :: "[i, i, [i,i,i]=>i] => i"