--- a/Nominal/NewAlpha.thy	Mon May 24 20:02:37 2010 +0100
+++ b/Nominal/NewAlpha.thy	Mon May 24 20:50:15 2010 +0100
@@ -181,7 +181,7 @@
 *}
 
 ML {*
-fun define_raw_alpha descr sorts bn_info bclausesss fvs fv_bns lthy =
+fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy =
 let
   val alpha_names = prefix_dt_names descr sorts "alpha_"
   val alpha_arg_tys = all_dtyps descr sorts
@@ -226,6 +226,4 @@
 end
 *}
 
-ML {* ProofContext.export_morphism *}
-
 end