src/HOL/thy_syntax.ML
changeset 8623 5668aaf41c36
parent 6642 732af87c0650
child 8657 b9475dad85ed
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Mar 30 19:44:11 2000 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Mar 30 19:45:18 2000 +0200
     1.3 @@ -221,12 +221,13 @@
     1.4    in
     1.5      ";\n\n\
     1.6      \local\n\
     1.7 +    \fun simpset() = Simplifier.simpset_of thy;\n\
     1.8      \val (thy, result) = thy |> RecdefPackage.add_recdef " ^ quote fid ^ " " ^ rel ^ "\n" ^
     1.9      axms_text ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\
    1.10      \in\n\
    1.11      \structure " ^ fid ^ " =\n\
    1.12      \struct\n\
    1.13 -    \  val {rules, induct, tcs} = result;\n\
    1.14 +    \  val {simps, induct, tcs} = result;\n\
    1.15      \end;\n\
    1.16      \val thy = thy;\n\
    1.17      \end;\n\