diff -r 7c09bd3227c5 -r 3da5f3f07d8b CookBook/Package/Ind_Interface.thy
--- a/CookBook/Package/Ind_Interface.thy	Fri Mar 13 12:21:44 2009 +0100
+++ b/CookBook/Package/Ind_Interface.thy	Fri Mar 13 16:57:16 2009 +0100
@@ -277,7 +277,7 @@
   
   @{ML [display] "Specification.read_specification:
   (Binding.binding * string option * mixfix) list ->  (*{variables}*)
-  (Attrib.binding * string list) list list ->  (*{rules}*)
+  (Attrib.binding * string list) list ->  (*{rules}*)
   local_theory ->
   (((Binding.binding * typ) * mixfix) list *
    (Attrib.binding * term list) list) *
@@ -315,8 +315,8 @@
 "Specification.read_specification
   [(Binding.name \"trcl\", NONE, NoSyn),
    (Binding.name \"r\", SOME \"'a \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)]
-  [[((Binding.name \"base\", []), [\"trcl r x x\"])],
-   [((Binding.name \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]]
+  [((Binding.name \"base\", []), [\"trcl r x x\"]),
+   ((Binding.name \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]
   @{context}"
 "((\<dots>,
   [(\<dots>,