# HG changeset patch
# User wenzelm
# Date 969039268 -7200
# Node ID fdead18501ca290ea98516bbd035dc545b1c6742
# Parent  09c65992894c093594cfbceb0414eb1725f69783
"hints" made keyword again;

diff -r 09c65992894c -r fdead18501ca src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Fri Sep 15 19:32:27 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Fri Sep 15 19:34:28 2000 +0200
@@ -329,6 +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_parsers [recdefP, defer_recdefP];
 
 end;