# HG changeset patch
# User blanchet
# Date 1398241407 -7200
# Node ID 54326fa7afe617e73f0836630e41e867cdfc8b7a
# Parent  c1507d5f46654d74278e00363b2b458e799e625b
qualify name

diff -r c1507d5f4665 -r 54326fa7afe6 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- 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;
diff -r c1507d5f4665 -r 54326fa7afe6 src/HOL/Transfer.thy
--- 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.