--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:27 2014 +0200
@@ -112,7 +112,9 @@
val fsB = map2 (curry Free) f_names f_TsB;
val As_fs = As ~~ fs;
- val size_bs = map (Binding.name o prefix size_N o Long_Name.base_name) T_names;
+ val size_bs =
+ map ((fn base => Binding.qualify false base (Binding.name (prefix size_N base))) o
+ Long_Name.base_name) T_names;
fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T'
| is_pair_C _ _ = false;
--- a/src/HOL/Transfer.thy Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Transfer.thy Wed Apr 23 10:23:27 2014 +0200
@@ -6,7 +6,7 @@
header {* Generic theorem transfer using relations *}
theory Transfer
-imports Hilbert_Choice Basic_BNFs BNF_FP_Base Metis Option
+imports Hilbert_Choice BNF_FP_Base Metis Option
begin
(* We include Option here altough it's not needed here.