--- a/Quot/QuotMain.thy	Wed Dec 09 15:29:36 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 15:35:21 2009 +0100
@@ -977,21 +977,6 @@
 *}
 
 ML {*
-fun make_inst3 lhs t =
-  let
-    val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
-    val _ $ (Abs (_, _, (_ $ g))) = 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;
-*}
-
-ML {*
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
    ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
@@ -1019,7 +1004,7 @@
            Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
          end handle _ => (* TODO handle only Bind | Error "make_inst" *)
          let
-           val (insp, inst) = make_inst3 (term_of (Thm.lhs_of te)) (term_of ctrm)
+           val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
            val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
          in
            MetaSimplifier.rewrite_rule (id_simps_get ctxt) td