# HG changeset patch
# User nipkow
# Date 954438318 -7200
# Node ID 5668aaf41c368b67d4ccaed2c1b4e575830dacaa
# Parent  870a58dd0ddda346973ab45e3496df10fc6a31d7
mod in recdef allows to access the correct simpset via simpset().

diff -r 870a58dd0ddd -r 5668aaf41c36 src/HOL/thy_syntax.ML
--- 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\