--- a/CookBook/Package/simple_inductive_package.ML	Fri Mar 13 12:21:44 2009 +0100
+++ b/CookBook/Package/simple_inductive_package.ML	Fri Mar 13 16:57:16 2009 +0100
@@ -198,7 +198,7 @@
 (* @chunk read_specification *)
 fun read_specification' vars specs lthy =
 let 
-  val specs' = map (fn (a, s) => [(a, [s])]) specs
+  val specs' = map (fn (a, s) => (a, [s])) specs
   val ((varst, specst), _) = 
                    Specification.read_specification vars specs' lthy
   val specst' = map (apsnd the_single) specst