1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 11:47:51 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 12:06:03 2012 +0200
     1.3 @@ -59,12 +59,8 @@
     1.4  
     1.5  fun resort_tfree S (TFree (s, _)) = TFree (s, S);
     1.6  
     1.7 -fun retype_free T (Free (s, _)) = Free (s, T);
     1.8 -
     1.9  val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
    1.10  
    1.11 -fun mk_predT T = T --> HOLogic.boolT;
    1.12 -
    1.13  fun mk_id T = Const (@{const_name id}, T --> T);
    1.14  
    1.15  fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));