--- 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