diff -r ed0c7b4a325d -r 8b0c9205da75 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Wed Mar 17 13:47:04 1999 +0100
+++ b/src/HOL/Induct/SList.thy	Wed Mar 17 13:47:34 1999 +0100
@@ -33,7 +33,7 @@
 
 
 typedef (List)
-  'a list = "list(range Leaf)" (list.NIL_I)
+  'a list = "list(range Leaf) :: 'a item set" (list.NIL_I)
 
   
 (*Declaring the abstract list constructors*)