mod in recdef allows to access the correct simpset via simpset().

--- a/src/HOL/thy_syntax.ML	Thu Mar 30 19:44:11 2000 +0200
+++ b/src/HOL/thy_syntax.ML	Thu Mar 30 19:45:18 2000 +0200
@@ -221,12 +221,13 @@
   in
     ";\n\n\
     \local\n\
+    \fun simpset() = Simplifier.simpset_of thy;\n\
     \val (thy, result) = thy |> RecdefPackage.add_recdef " ^ quote fid ^ " " ^ rel ^ "\n" ^
     axms_text ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\
     \in\n\
     \structure " ^ fid ^ " =\n\
     \struct\n\
-    \  val {rules, induct, tcs} = result;\n\
+    \  val {simps, induct, tcs} = result;\n\
     \end;\n\
     \val thy = thy;\n\
     \end;\n\