--- a/QuotMain.thy	Wed Dec 02 14:37:21 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 16:12:41 2009 +0100
@@ -22,13 +22,15 @@
   let
     val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
     val _ $ (Abs (_, _, g)) = t;
-    fun mk_abs i t =
+    
+  fun mk_abs i t =
       if incr_boundvars i u aconv t then Bound i
       else (case t of
         t1 $ t2 => mk_abs i t1 $ mk_abs i t2
       | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
       | Bound j => if i = j then error "make_inst" else t
       | _ => t);
+
   in (f, Abs ("x", T, mk_abs 0 g)) end;
 *}