do not expose details of internal data structures for composition of BNFs
authortraytel
Thu Oct 04 17:16:55 2012 +0200 (2012-10-04)
changeset 497133d07ddf70f8b
parent 49699 1301ed115729
child 49714 2c7c32f34220
do not expose details of internal data structures for composition of BNFs
src/HOL/BNF/Tools/bnf_comp.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Thu Oct 04 13:56:32 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Thu Oct 04 17:16:55 2012 +0200
     1.3 @@ -13,10 +13,6 @@
     1.4  
     1.5    type unfold_set
     1.6    val empty_unfolds: unfold_set
     1.7 -  val map_unfolds_of: unfold_set -> thm list
     1.8 -  val rel_unfolds_of: unfold_set -> thm list
     1.9 -  val set_unfoldss_of: unfold_set -> thm list list
    1.10 -  val srel_unfolds_of: unfold_set -> thm list
    1.11  
    1.12    val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
    1.13      ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
    1.14 @@ -64,11 +60,6 @@
    1.15    add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf)
    1.16      (srel_def_of_bnf bnf);
    1.17  
    1.18 -val map_unfolds_of = #map_unfolds;
    1.19 -val set_unfoldss_of = #set_unfoldss;
    1.20 -val rel_unfolds_of = #rel_unfolds;
    1.21 -val srel_unfolds_of = #srel_unfolds;
    1.22 -
    1.23  val bdTN = "bdT";
    1.24  
    1.25  fun mk_killN n = "_kill" ^ string_of_int n;
    1.26 @@ -603,10 +594,10 @@
    1.27      val (Bs, _) = apfst (map TFree)
    1.28        (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
    1.29  
    1.30 -    val map_unfolds = map_unfolds_of unfold_set;
    1.31 -    val set_unfoldss = set_unfoldss_of unfold_set;
    1.32 -    val rel_unfolds = rel_unfolds_of unfold_set;
    1.33 -    val srel_unfolds = srel_unfolds_of unfold_set;
    1.34 +    val map_unfolds = #map_unfolds unfold_set;
    1.35 +    val set_unfoldss = #set_unfoldss unfold_set;
    1.36 +    val rel_unfolds = #rel_unfolds unfold_set;
    1.37 +    val srel_unfolds = #srel_unfolds unfold_set;
    1.38  
    1.39      val expand_maps =
    1.40        fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);