removed dead code
authorblanchet
Mon, 11 Nov 2013 18:13:17 +0100
changeset 54302 880e5417b800
parent 54301 e0943a2ee400
child 54303 4f55054d197c
removed dead code
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