1.1 --- a/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 20:07:00 2012 +0100
     1.2 +++ b/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 22:08:53 2012 +0100
     1.3 @@ -6,7 +6,10 @@
     1.4  
     1.5  theory Old_Recdef
     1.6  imports Wfrec
     1.7 -keywords "recdef" :: thy_decl and "permissive" "congs" "hints"
     1.8 +keywords
     1.9 +  "recdef" "defer_recdef" :: thy_decl and
    1.10 +  "recdef_tc" :: thy_goal and
    1.11 +  "permissive" "congs" "hints"
    1.12  uses
    1.13    ("~~/src/HOL/Tools/TFL/casesplit.ML")
    1.14    ("~~/src/HOL/Tools/TFL/utils.ML")