diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Feb 19 08:34:32 2014 +0100
+++ b/src/HOL/Inductive.thy	Wed Feb 19 08:34:33 2014 +0100
@@ -11,7 +11,7 @@
   "inductive_cases" "inductive_simps" :: thy_script and "monos" and
   "print_inductives" :: diag and
   "rep_datatype" :: thy_goal and
-  "old_primrec" :: thy_decl
+  "primrec" :: thy_decl
 begin
 
 subsection {* Least and greatest fixed points *}
@@ -277,6 +277,9 @@
 ML_file "Tools/Datatype/datatype_codegen.ML"
 ML_file "Tools/Datatype/primrec.ML"
 
+ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
+ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
+
 text{* Lambda-abstractions with pattern matching: *}
 
 syntax