# HG changeset patch
# User wenzelm
# Date 969042156 -7200
# Node ID 566c6b90637089ed8cac4ee68b9470985b0ef1a2
# Parent  09bf8fcd1c6eb7a0fea8b0a1f0674c431b899799
added "congs" keyword;

diff -r 09bf8fcd1c6e -r 566c6b906370 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Fri Sep 15 20:22:00 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Fri Sep 15 20:22:36 2000 +0200
@@ -329,7 +329,7 @@
   OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
     (defer_recdef_decl >> Toplevel.theory);
 
-val _ = OuterSyntax.add_keywords ["hints"];
+val _ = OuterSyntax.add_keywords ["congs", "hints"];
 val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP];
 
 end;