--- a/src/HOL/BNF/BNF_Def.thy Wed Nov 13 09:37:00 2013 +0100 +++ b/src/HOL/BNF/BNF_Def.thy Wed Nov 13 10:53:36 2013 +0100 @@ -202,5 +202,4 @@ ML_file "Tools/bnf_def_tactics.ML" ML_file "Tools/bnf_def.ML" - end