use base names, not full names
authorblanchet
Mon Apr 29 14:06:37 2013 +0200 (2013-04-29)
changeset 518165f1dec4297da
parent 51815 efacb9b99865
child 51817 6b82042690b5
use base names, not full names
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:52:14 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 14:06:37 2013 +0200
     1.3 @@ -75,11 +75,10 @@
     1.4      in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
     1.5  
     1.6  fun add_components_of_typ (Type (s, Ts)) =
     1.7 -    fold add_components_of_typ Ts
     1.8 -    #> cons s
     1.9 +    fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
    1.10    | add_components_of_typ _ = I;
    1.11  
    1.12 -fun name_of_typ T = space_implode "_" (add_components_of_typ T []);
    1.13 +fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
    1.14  
    1.15  fun exists_subtype_in Ts = exists_subtype (member (op =) Ts);
    1.16  
    1.17 @@ -211,12 +210,12 @@
    1.18      val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
    1.19      val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
    1.20  
    1.21 -    val fp_T_names = map name_of_typ fpTs;
    1.22 +    val fp_b_names = map base_name_of_typ fpTs;
    1.23  
    1.24      val (((ps, ps'), us'), names_lthy) =
    1.25        lthy
    1.26        |> mk_Frees' "P" (map mk_pred1T fpTs)
    1.27 -      ||>> Variable.variant_fixes fp_T_names;
    1.28 +      ||>> Variable.variant_fixes fp_b_names;
    1.29  
    1.30      val us = map2 (curry Free) us' fpTs;
    1.31  
    1.32 @@ -368,7 +367,7 @@
    1.33      val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
    1.34      val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
    1.35  
    1.36 -    val fp_T_names = map name_of_typ fpTs;
    1.37 +    val fp_b_names = map base_name_of_typ fpTs;
    1.38  
    1.39      val discss = map (map (mk_disc_or_sel As) o #1) ctr_wrap_ress;
    1.40      val selsss = map (map (map (mk_disc_or_sel As)) o #2) ctr_wrap_ress;
    1.41 @@ -380,8 +379,8 @@
    1.42      val (((rs, us'), vs'), names_lthy) =
    1.43        lthy
    1.44        |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)
    1.45 -      ||>> Variable.variant_fixes fp_T_names
    1.46 -      ||>> Variable.variant_fixes (map (suffix "'") fp_T_names);
    1.47 +      ||>> Variable.variant_fixes fp_b_names
    1.48 +      ||>> Variable.variant_fixes (map (suffix "'") fp_b_names);
    1.49  
    1.50      val us = map2 (curry Free) us' fpTs;
    1.51      val udiscss = map2 (map o rapp) us discss;
    1.52 @@ -466,7 +465,7 @@
    1.53          flat (map2 append disc_concls ctr_concls)
    1.54        end;
    1.55  
    1.56 -    val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_T_names);
    1.57 +    val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
    1.58      val coinduct_conclss =
    1.59        map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
    1.60