1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  val meta_mp = @{thm meta_mp};
     1.5  val meta_spec = @{thm meta_spec};
     1.6  
     1.7 -fun squash_spurious_fs lthy thm =
     1.8 +fun smash_spurious_fs lthy thm =
     1.9    let
    1.10      val spurious_fs =
    1.11        Term.add_vars (prop_of thm) []
    1.12 @@ -41,7 +41,7 @@
    1.13      Drule.cterm_instantiate cxs thm
    1.14    end;
    1.15  
    1.16 -val squash_spurious_fs_tac = PRIMITIVE o squash_spurious_fs;
    1.17 +val smash_spurious_fs_tac = PRIMITIVE o smash_spurious_fs;
    1.18  
    1.19  fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
    1.20    Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
    1.21 @@ -89,7 +89,7 @@
    1.22    TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
    1.23  
    1.24  fun mk_induct_prelude_tac ctxt ctr_defs fld_induct' =
    1.25 -  Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN squash_spurious_fs_tac ctxt;
    1.26 +  Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt;
    1.27  
    1.28  fun mk_induct_prepare_prem_tac n m k =
    1.29    EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,