diff -r 82db9ad610b9 -r 8081087096ad src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Mon Sep 01 16:17:46 2014 +0200 +++ b/src/HOL/BNF_FP_Base.thy Mon Sep 01 16:17:46 2014 +0200 @@ -205,8 +205,8 @@ ML_file "Tools/BNF/bnf_fp_n2m.ML" ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML" -ML_file "Tools/Function/size.ML" -setup Size.setup +ML_file "Tools/Function/old_size.ML" +setup Old_Size.setup lemma size_bool[code]: "size (b\bool) = 0" by (cases b) auto