--- a/Nominal/NewFv.thy	Fri Apr 30 13:57:59 2010 +0200
+++ b/Nominal/NewFv.thy	Fri Apr 30 14:48:13 2010 +0200
@@ -271,17 +271,20 @@
     Function.prove_termination NONE
       (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
 
-  val (info, lthy') = Function.add_function all_fv_names all_fv_eqs
+  val (_, lthy') = Function.add_function all_fv_names all_fv_eqs
     Function_Common.default_config pat_completeness_auto lthy
 
-  val lthy'' = prove_termination (Local_Theory.restore lthy')
+  val (info, lthy'') = prove_termination (Local_Theory.restore lthy')
+
+  val {fs, simps, ...} = info;
 
   val morphism = ProofContext.export_morphism lthy'' lthy
-  val fv_frees_exp = map (Morphism.term morphism) fv_frees
-  val fv_bns_exp = map (Morphism.term morphism) fv_bns
+  val fs_exp = map (Morphism.term morphism) fs
 
+  val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
+  val simps_exp = Morphism.fact morphism (the simps)
 in
-  ((fv_frees_exp, fv_bns_exp), @{thms refl}, lthy'')
+  ((fv_frees_exp, fv_bns_exp), simps_exp, lthy'')
 end
 *}