# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259770604 -3600
# Node ID 7c26b31d2371a889ce536184aef51c1d1dc3af42
# Parent  4efb104514f7ea9129fb45b04b0d0ee7bc06ea3c# Parent  123aeffbd65efc6409343c56a98b75bffa4d3043
merge

diff -r 4efb104514f7 -r 7c26b31d2371 QuotMain.thy
--- a/QuotMain.thy	Wed Dec 02 17:15:36 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 17:16:44 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;
 *}