1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 05:29:21 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 06:27:36 2012 +0200
     1.3 @@ -369,7 +369,6 @@
     1.4              (case_binder :: ctr_binders) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
     1.5            ||> `Local_Theory.restore;
     1.6  
     1.7 -        (*transforms defined frees into consts (and more)*)
     1.8          val phi = Proof_Context.export_morphism lthy lthy';
     1.9  
    1.10          val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
    1.11 @@ -446,7 +445,6 @@
    1.12                  #>> apsnd snd) binders specs
    1.13                ||> `Local_Theory.restore;
    1.14  
    1.15 -            (*transforms defined frees into consts (and more)*)
    1.16              val phi = Proof_Context.export_morphism lthy lthy';
    1.17  
    1.18              val [iter_def, rec_def] = map (Morphism.thm phi) defs;
    1.19 @@ -490,7 +488,6 @@
    1.20                  #>> apsnd snd) binders specs
    1.21                ||> `Local_Theory.restore;
    1.22  
    1.23 -            (*transforms defined frees into consts (and more)*)
    1.24              val phi = Proof_Context.export_morphism lthy lthy';
    1.25  
    1.26              val [coiter_def, corec_def] = map (Morphism.thm phi) defs;