src/HOL/Tools/Quotient/quotient_term.ML

-(*  Title:      quotient_term.thy
+(*  Title:      HOL/Tools/Quotient/quotient_term.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Constructs terms corresponding to goals from
-    lifting theorems to quotient types.
+Constructs terms corresponding to goals from lifting theorems to
+quotient types.
 *)
 
 signature QUOTIENT_TERM =
 sig
   exception LIFT_MATCH of string

       | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
 in
   lift_aux t
 end
 
-
 end; (* structure *)
-
-
-