
diff -r b5965890e54d -r ef0a5fd30f3b src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Inductive.thy	Wed Dec 28 17:22:16 2016 +0100
@@ -519,9 +519,8 @@
 ML_file "Tools/Old_Datatype/old_datatype_data.ML"
 ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
 ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
+ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
 ML_file "Tools/Old_Datatype/old_primrec.ML"
-
-ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
 ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
 
 text \<open>Lambda-abstractions with pattern matching:\<close>




