src/HOL/Tools/BNF/bnf_comp.ML
changeset 55937 18e52e8c6300
parent 55935 8f20d09d294e
child 56010 abf4879d39f1
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 06 14:15:09 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 06 14:25:55 2014 +0100
     1.3 @@ -109,7 +109,6 @@
     1.4  fun mk_permuteN src dest =
     1.5    "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
     1.6  
     1.7 -val id_bnf_comp_def = @{thm id_bnf_comp_def}
     1.8  
     1.9  (*copied from Envir.expand_term_free*)
    1.10  fun expand_term_const defs =
    1.11 @@ -118,6 +117,10 @@
    1.12      val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
    1.13    in Envir.expand_term get end;
    1.14  
    1.15 +val id_bnf_comp_def = @{thm id_bnf_comp_def};
    1.16 +val expand_id_bnf_comp_def =
    1.17 +  expand_term_const [Thm.prop_of id_bnf_comp_def |> Logic.dest_equals];
    1.18 +
    1.19  fun is_sum_prod_natLeq (Const (@{const_name csum}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
    1.20    | is_sum_prod_natLeq (Const (@{const_name cprod}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
    1.21    | is_sum_prod_natLeq t = t aconv @{term natLeq};
    1.22 @@ -342,8 +345,7 @@
    1.23  
    1.24      val phi =
    1.25        Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_comp_def])
    1.26 -      $> Morphism.term_morphism "BNF" (Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy')
    1.27 -        [id_bnf_comp_def] []);
    1.28 +      $> Morphism.term_morphism "BNF" expand_id_bnf_comp_def;
    1.29  
    1.30      val bnf'' = morph_bnf phi bnf';
    1.31    in
    1.32 @@ -761,10 +763,8 @@
    1.33  
    1.34      val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
    1.35        |> mk_Frees' "f" (map2 (curry op -->) As Bs)
    1.36 -      ||>> mk_Frees' "R" (map2 mk_pred2T As Bs)
    1.37 +      ||>> mk_Frees' "R" (map2 mk_pred2T As Bs);
    1.38  
    1.39 -    val expand_id_bnf_comp_def =
    1.40 -      expand_term_const [Thm.prop_of id_bnf_comp_def |> Logic.dest_equals]
    1.41      val map_unfolds = #map_unfolds unfold_set;
    1.42      val set_unfoldss = #set_unfoldss unfold_set;
    1.43      val rel_unfolds = #rel_unfolds unfold_set;