qualify name
authorblanchet
Wed Apr 23 10:23:27 2014 +0200 (2014-04-23)
changeset 5665454326fa7afe6
parent 56653 c1507d5f4665
child 56655 34f2fe40dc7b
qualify name
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Apr 23 10:23:27 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Apr 23 10:23:27 2014 +0200
     1.3 @@ -112,7 +112,9 @@
     1.4      val fsB = map2 (curry Free) f_names f_TsB;
     1.5      val As_fs = As ~~ fs;
     1.6  
     1.7 -    val size_bs = map (Binding.name o prefix size_N o Long_Name.base_name) T_names;
     1.8 +    val size_bs =
     1.9 +      map ((fn base => Binding.qualify false base (Binding.name (prefix size_N base))) o
    1.10 +        Long_Name.base_name) T_names;
    1.11  
    1.12      fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T'
    1.13        | is_pair_C _ _ = false;
     2.1 --- a/src/HOL/Transfer.thy	Wed Apr 23 10:23:27 2014 +0200
     2.2 +++ b/src/HOL/Transfer.thy	Wed Apr 23 10:23:27 2014 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* Generic theorem transfer using relations *}
     2.5  
     2.6  theory Transfer
     2.7 -imports Hilbert_Choice Basic_BNFs BNF_FP_Base Metis Option
     2.8 +imports Hilbert_Choice BNF_FP_Base Metis Option
     2.9  begin
    2.10  
    2.11  (* We include Option here altough it's not needed here.