# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259766761 -3600
# Node ID 123aeffbd65efc6409343c56a98b75bffa4d3043
# Parent  74348dc2f8bb6ca3f8f6b512fcda01fb41075fa1
merged

diff -r 74348dc2f8bb -r 123aeffbd65e QuotMain.thy
--- 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;
 *}