# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272432057 -7200
# Node ID 9ae5380c828a057f357d6a77ad07f125755fd82e
# Parent  98303b78fb64ac432cc9f5f0fff345417e66dd11
white spaces

diff -r 98303b78fb64 -r 9ae5380c828a Nominal/NewFv.thy
--- 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;