--- a/Nominal/NewFv.thy	Wed Apr 28 07:09:11 2010 +0200
+++ b/Nominal/NewFv.thy	Wed Apr 28 07:20:57 2010 +0200
@@ -77,8 +77,8 @@
 ML {*
 fun setify x =
   if fastype_of x = @{typ "atom list"} 
-    then @{term "set::atom list \<Rightarrow> atom set"} $ x 
-    else x
+  then @{term "set::atom list \<Rightarrow> atom set"} $ x 
+  else x
 *}
 
 ML {*
@@ -131,8 +131,7 @@
 *}
 
 ML {*
-fun fv_bn thy dt_descr sorts fv_frees
-  bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) =
+fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) =
 let
   fun fv_bn_constr (cname, dts) (args_in_bn, bml) =
   let
@@ -218,7 +217,7 @@
 *}
 
 ML {*
-fun define_raw_fv (dt_info : Datatype_Aux.info)  bn_funs bclauses lthy =
+fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclauses lthy =
 let
   val thy = ProofContext.theory_of lthy;
   val {descr as dt_descr, sorts, ...} = dt_info;