src/HOL/Tools/BNF/bnf_comp.ML

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 06 13:36:50 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 06 14:14:54 2014 +0100
@@ -56,8 +56,8 @@
 open BNF_Tactics
 open BNF_Comp_Tactics
 
-val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
-val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
+val ID_bnf = the (bnf_of @{context} "BNF_Comp.ID");
+val DEADID_bnf = the (bnf_of @{context} "BNF_Comp.DEADID");
 
 type comp_cache = (bnf * (typ list * typ list)) Typtab.table;
 
@@ -109,6 +109,8 @@
 fun mk_permuteN src dest =
   "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
 
+val id_bnf_comp_def = @{thm id_bnf_comp_def}
+
 (*copied from Envir.expand_term_free*)
 fun expand_term_const defs =
   let
@@ -339,9 +341,9 @@
         Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
 
     val phi =
-      Morphism.thm_morphism "BNF" (unfold_thms lthy' @{thms id_bnf_comp_def})
+      Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_comp_def])
       $> Morphism.term_morphism "BNF" (Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy')
-        @{thms id_bnf_comp_def[abs_def]} []);
+        [id_bnf_comp_def] []);
 
     val bnf'' = morph_bnf phi bnf';
   in
@@ -761,19 +763,21 @@
       |> mk_Frees' "f" (map2 (curry op -->) As Bs)
       ||>> mk_Frees' "R" (map2 mk_pred2T As Bs)
 
+    val expand_id_bnf_comp_def =
+      expand_term_const [Thm.prop_of id_bnf_comp_def |> Logic.dest_equals]
     val map_unfolds = #map_unfolds unfold_set;
     val set_unfoldss = #set_unfoldss unfold_set;
     val rel_unfolds = #rel_unfolds unfold_set;
 
-    val expand_maps =
+    val expand_maps = expand_id_bnf_comp_def o
       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
     val expand_sets =
       fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
-    val expand_rels =
+    val expand_rels = expand_id_bnf_comp_def o
       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
-    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) map_unfolds;
+    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: map_unfolds);
     fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
-    fun unfold_rels ctxt = unfold_thms ctxt rel_unfolds;
+    fun unfold_rels ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: rel_unfolds);
     fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
 
     val repTA = mk_T_of_bnf Ds As bnf;
@@ -854,7 +858,7 @@
 
     val bnf_wits = map (fn (I, t) =>
         fold Term.absdummy (map (nth As) I)
-          (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
+          (AbsA $ Term.list_comb (expand_id_bnf_comp_def t, map Bound (0 upto length I - 1))))
       (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
     fun wit_tac ctxt = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN