src/HOL/Tools/recdef_package.ML
changeset 8734 b456aba346a6
parent 8711 00ec2ba9174d
child 9640 8c6cf4f01644
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Apr 18 00:49:49 2000 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Apr 18 14:54:08 2000 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4    OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
     1.5      (defer_recdef_decl >> Toplevel.theory);
     1.6  
     1.7 -val _ = OuterSyntax.add_keywords ["congs", "simpset"];
     1.8 +val _ = OuterSyntax.add_keywords ["congs"];
     1.9  val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP];
    1.10  
    1.11  end;