src/HOL/BNF/Tools/bnf_comp.ML
changeset 54742 7a86358a3c0b
parent 54421 632be352a5a3
child 54841 af71b753c459
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -590,10 +590,10 @@
     1.4        fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
     1.5      val expand_rels =
     1.6        fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
     1.7 -    val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
     1.8 -    val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
     1.9 -    val unfold_rels = unfold_thms lthy rel_unfolds;
    1.10 -    val unfold_all = unfold_sets o unfold_maps o unfold_rels;
    1.11 +    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) map_unfolds;
    1.12 +    fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
    1.13 +    fun unfold_rels ctxt = unfold_thms ctxt rel_unfolds;
    1.14 +    fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
    1.15      val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
    1.16      val bnf_sets = map (expand_maps o expand_sets)
    1.17        (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
    1.18 @@ -627,7 +627,7 @@
    1.19        map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
    1.20  
    1.21      fun mk_tac thm {context = ctxt, prems = _} =
    1.22 -      (rtac (unfold_all thm) THEN'
    1.23 +      (rtac (unfold_all ctxt thm) THEN'
    1.24        SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
    1.25  
    1.26      val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf))
    1.27 @@ -638,7 +638,8 @@
    1.28  
    1.29      val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
    1.30  
    1.31 -    fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
    1.32 +    fun wit_tac {context = ctxt, prems = _} =
    1.33 +      mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
    1.34  
    1.35      val (bnf', lthy') =
    1.36        bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)