1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:11 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:11 2012 +0200
     1.3 @@ -32,14 +32,13 @@
     1.4  
     1.5  fun smash_spurious_fs lthy thm =
     1.6    let
     1.7 -    val spurious_fs =
     1.8 +    val fs =
     1.9        Term.add_vars (prop_of thm) []
    1.10        |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false);
    1.11 -    val cxs =
    1.12 -      map (fn s as (_, T) =>
    1.13 -        (certify lthy (Var s), certify lthy (id_abs (domain_type T)))) spurious_fs;
    1.14 +    val cfs =
    1.15 +      map (fn f as (_, T) => (certify lthy (Var f), certify lthy (id_abs (domain_type T)))) fs;
    1.16    in
    1.17 -    Drule.cterm_instantiate cxs thm
    1.18 +    Drule.cterm_instantiate cfs thm
    1.19    end;
    1.20  
    1.21  val smash_spurious_fs_tac = PRIMITIVE o smash_spurious_fs;
    1.22 @@ -113,7 +112,7 @@
    1.23  val induct_prem_prem_thms_delayed =
    1.24    @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    1.25  
    1.26 -(* TODO: Get rid of the "auto_tac" (or at least use a naked context) *)
    1.27 +(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
    1.28  fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
    1.29    | mk_induct_prem_prem_endgame_tac ctxt qq =
    1.30      REPEAT_DETERM_N qq o
    1.31 @@ -123,7 +122,7 @@
    1.32  
    1.33  fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =
    1.34    EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    1.35 -      [select_prem_tac nn (dtac meta_spec) kk, rotate_tac ~1 (*FIXME: needed?*), etac meta_mp,
    1.36 +      [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    1.37         SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* FIXME: ### why on a line of its own? *)
    1.38         SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
    1.39         SELECT_GOAL (Local_Defs.unfold_tac ctxt