--- a/Nominal/nominal_dt_rawfuns.ML	Tue Aug 17 18:00:55 2010 +0800
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Aug 17 18:17:53 2010 +0800
@@ -240,12 +240,12 @@
 
   val morphism = ProofContext.export_morphism lthy'' lthy
   val fs_exp = map (Morphism.term morphism) fs
-
+  val simps_exp = map (Morphism.thm morphism) (the simps)
+  val inducts_exp = map (Morphism.thm morphism) (the inducts)
   val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
-  val simps_exp = map (Morphism.thm morphism) (the simps)
-  val fv_bns_inducts_exp = map (Morphism.thm morphism) (the inducts)
+  
 in
-  (fv_frees_exp, fv_bns_exp, simps_exp, fv_bns_inducts_exp, lthy'')
+  (fv_frees_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'')
 end