diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Fri Sep 10 09:17:40 2010 +0800
@@ -20,11 +20,13 @@
     (string * term * mixfix) list -> local_theory -> local_theory
 
   val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context
+
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
 struct
 
+
 (* defines the quotient types *)
 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
 let
@@ -86,7 +88,7 @@
 end
 
 
-(* lifts a theorem and cleans all "_raw" instances 
+(* lifts a theorem and cleans all "_raw" parts
    from variable names *)
 
 local
@@ -126,6 +128,5 @@
         #> unraw_vars_thm
         #> Drule.zero_var_indexes) thms, ctxt)
 
-
 end (* structure *)