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 @@ -53,7 +53,7 @@
     1.4    Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
     1.5  
     1.6  fun mk_induct_tac ctxt =
     1.7 -  Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)(*###*);
     1.8 +  Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt) (* FIXME: TODO *);
     1.9  
    1.10  val iter_like_thms =
    1.11    @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps