--- a/Nominal/nominal_dt_rawfuns.ML	Wed Jun 22 14:14:54 2011 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu Jun 23 11:30:39 2011 +0100
@@ -281,15 +281,19 @@
 
     val (info, lthy'') = prove_termination_fun size_simps (Local_Theory.restore lthy')
  
-    val {fs, simps, inducts, ...} = info;
+    val {fs, simps, inducts, ...} = info; 
 
     val morphism = ProofContext.export_morphism lthy'' lthy
     val simps_exp = map (Morphism.thm morphism) (the simps)
     val inducts_exp = map (Morphism.thm morphism) (the inducts)
-
+    
     val (fvs', fv_bns') = chop (length fv_frees) fs
+
+    (* grafting the types so that they coincide with the input into the function package *)
+    val fvs'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fvs' fv_tys
+    val fv_bns'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fv_bns' fv_bn_tys
   in
-    (fvs', fv_bns', simps_exp, inducts_exp, lthy'')
+    (fvs'', fv_bns'', simps_exp, inducts_exp, lthy'')
   end