1.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Wed Sep 12 02:05:03 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Wed Sep 12 02:05:04 2012 +0200
     1.3 @@ -284,7 +284,7 @@
     1.4  
     1.5  (* Killing live variables *)
     1.6  
     1.7 -fun killN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
     1.8 +fun kill_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
     1.9    let
    1.10      val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf);
    1.11      val live = live_of_bnf bnf;
    1.12 @@ -323,12 +323,12 @@
    1.13        Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    1.14        rtac refl 1;
    1.15      fun map_cong_tac {context, ...} =
    1.16 -      mk_killN_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
    1.17 +      mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
    1.18      val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
    1.19 -    fun bd_card_order_tac _ = mk_killN_bd_card_order_tac n (bd_card_order_of_bnf bnf);
    1.20 -    fun bd_cinfinite_tac _ = mk_killN_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
    1.21 +    fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
    1.22 +    fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
    1.23      val set_bd_tacs =
    1.24 -      map (fn thm => fn _ => mk_killN_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
    1.25 +      map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
    1.26          (drop n (set_bd_of_bnf bnf));
    1.27  
    1.28      val in_alt_thm =
    1.29 @@ -337,11 +337,11 @@
    1.30          val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
    1.31          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
    1.32        in
    1.33 -        Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation
    1.34 +        Skip_Proof.prove lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
    1.35        end;
    1.36  
    1.37      fun in_bd_tac _ =
    1.38 -      mk_killN_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf)
    1.39 +      mk_kill_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf)
    1.40          (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
    1.41      fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
    1.42  
    1.43 @@ -383,7 +383,7 @@
    1.44  
    1.45  (* Adding dummy live variables *)
    1.46  
    1.47 -fun liftN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
    1.48 +fun lift_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
    1.49    let
    1.50      val b = Binding.prefix_name (mk_liftN n) (name_of_bnf bnf);
    1.51      val live = live_of_bnf bnf;
    1.52 @@ -431,7 +431,7 @@
    1.53        if ! quick_and_dirty then
    1.54          replicate (n + live) (K all_tac)
    1.55        else
    1.56 -        replicate n (K (mk_liftN_set_bd_tac (bd_Card_order_of_bnf bnf))) @
    1.57 +        replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @
    1.58          (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
    1.59  
    1.60      val in_alt_thm =
    1.61 @@ -440,10 +440,10 @@
    1.62          val in_alt = mk_in (drop n Asets) bnf_sets T;
    1.63          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
    1.64        in
    1.65 -        Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation
    1.66 +        Skip_Proof.prove lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation
    1.67        end;
    1.68  
    1.69 -    fun in_bd_tac _ = mk_liftN_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
    1.70 +    fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
    1.71      fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
    1.72  
    1.73      val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac,
    1.74 @@ -555,11 +555,11 @@
    1.75  fun permute_and_kill qualify n src dest bnf =
    1.76    bnf
    1.77    |> permute_bnf qualify src dest
    1.78 -  #> uncurry (killN_bnf qualify n);
    1.79 +  #> uncurry (kill_bnf qualify n);
    1.80  
    1.81  fun lift_and_permute qualify n src dest bnf =
    1.82    bnf
    1.83 -  |> liftN_bnf qualify n
    1.84 +  |> lift_bnf qualify n
    1.85    #> uncurry (permute_bnf qualify src dest);
    1.86  
    1.87  fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy =