# HG changeset patch
# User traytel
# Date 1349363815 -7200
# Node ID 3d07ddf70f8b7e124075db0716b53a0584e05daf
# Parent  1301ed1157298c91d70d823aa822c28821ad36ef
do not expose details of internal data structures for composition of BNFs

diff -r 1301ed115729 -r 3d07ddf70f8b src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Thu Oct 04 13:56:32 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Thu Oct 04 17:16:55 2012 +0200
@@ -13,10 +13,6 @@
 
   type unfold_set
   val empty_unfolds: unfold_set
-  val map_unfolds_of: unfold_set -> thm list
-  val rel_unfolds_of: unfold_set -> thm list
-  val set_unfoldss_of: unfold_set -> thm list list
-  val srel_unfolds_of: unfold_set -> thm list
 
   val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
     ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
@@ -64,11 +60,6 @@
   add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf)
     (srel_def_of_bnf bnf);
 
-val map_unfolds_of = #map_unfolds;
-val set_unfoldss_of = #set_unfoldss;
-val rel_unfolds_of = #rel_unfolds;
-val srel_unfolds_of = #srel_unfolds;
-
 val bdTN = "bdT";
 
 fun mk_killN n = "_kill" ^ string_of_int n;
@@ -603,10 +594,10 @@
     val (Bs, _) = apfst (map TFree)
       (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
 
-    val map_unfolds = map_unfolds_of unfold_set;
-    val set_unfoldss = set_unfoldss_of unfold_set;
-    val rel_unfolds = rel_unfolds_of unfold_set;
-    val srel_unfolds = srel_unfolds_of unfold_set;
+    val map_unfolds = #map_unfolds unfold_set;
+    val set_unfoldss = #set_unfoldss unfold_set;
+    val rel_unfolds = #rel_unfolds unfold_set;
+    val srel_unfolds = #srel_unfolds unfold_set;
 
     val expand_maps =
       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);