diff -r eb93bc67d361 -r 14e186d2dd3a src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Sep 09 22:33:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Sep 09 23:54:39 2014 +0200
@@ -180,8 +180,10 @@
         if T = fpT andalso kk' <> kk then
           mutual_self_call (nth callers kk)
             (the (find_first (not o null o get_indices callers) calls))
+        else if T = nth fpTs kk' then
+          nth Xs kk'
         else
-          nth Xs kk'
+          freeze_fpTs_type_based_default T
       | _ => incompatible_calls calls);
 
     fun freeze_fpTs_map kk (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls))