# HG changeset patch
# User blanchet
# Date 1384189997 -3600
# Node ID 880e5417b800dbc9e175f7afcc64021cdbadc52a
# Parent  e0943a2ee400e0b435786679a5c0723779ceafbf
removed dead code

diff -r e0943a2ee400 -r 880e5417b800 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 17:59:41 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 18:13:17 2013 +0100
@@ -134,9 +134,9 @@
 
     val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
     val mapss = map (of_fp_sugar #mapss) fp_sugars0;
-    val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
+    val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
 
-    val ctrss = map #ctrs ctr_sugars0;
+    val ctrss = map #ctrs ctr_sugars;
     val ctr_Tss = map (map fastype_of) ctrss;
 
     val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
@@ -214,13 +214,6 @@
               (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
           |>> split_list;
 
-        val rho = tvar_subst thy ctr_Ts fpTs;
-        val ctr_sugar_phi = Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
-            (Morphism.term_morphism (Term.subst_TVars rho));
-        val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;
-
-        val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
-
         val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
               sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
           if fp = Least_FP then