--- a/QuotMain.thy	Wed Dec 02 11:30:40 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 12:07:54 2009 +0100
@@ -774,7 +774,7 @@
   Subgoal.FOCUS (fn {concl, ...} =>
   let
     val pat = Drule.strip_imp_concl (cprop_of thm)
-    val insts = Thm.match (pat, concl)
+    val insts = Thm.first_order_match (pat, concl)
   in
     rtac (Drule.instantiate insts thm) 1
   end
@@ -865,7 +865,7 @@
           let
             val (asmf, asma) = find_qt_asm (map term_of asms);
             val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
-            val insts = Thm.match (pat, concl)
+            val insts = Thm.first_order_match (pat, concl)
           in
             if (fastype_of asmf) = (fastype_of f)
             then no_tac
@@ -951,7 +951,12 @@
 
 ML {* fun dest_comb (f $ a) = (f, a) *}
 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
-ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *}
+(* TODO: Can this be done easier? *)
+ML {*
+fun unlam t =
+  case t of
+    (Abs a) => snd (Term.dest_abs a)
+  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))  *}
 
 ML {*
 fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 =