# HG changeset patch
# User wenzelm
# Date 956062448 -7200
# Node ID b456aba346a6fda41009d63eeb6c3ed561ee3f98
# Parent  3213613a775a0b1edf4bb99b14b43b42920504a8
removed obsolete "simpset" keyword;

diff -r 3213613a775a -r b456aba346a6 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue Apr 18 00:49:49 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Tue Apr 18 14:54:08 2000 +0200
@@ -163,7 +163,7 @@
   OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
     (defer_recdef_decl >> Toplevel.theory);
 
-val _ = OuterSyntax.add_keywords ["congs", "simpset"];
+val _ = OuterSyntax.add_keywords ["congs"];
 val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP];
 
 end;