--- a/QuotMain.thy	Wed Oct 21 18:30:42 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 01:15:01 2009 +0200
@@ -659,7 +659,7 @@
        let 
           val ty1 = fastype_of trm
        in
-         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) (Abs (x, T, t)))    
+         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm)    
        end
   | Const (@{const_name "All"}, ty) $ t =>
        let 
@@ -1009,13 +1009,13 @@
   done
 
 ML {*
-fun instantiate_tac thm = (Subgoal.FOCUS (fn {concl, context, ...} =>
+fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, context, ...} =>
 let
- val pat = cterm_of (ProofContext.theory_of context) (concl_of thm)
- val insts = Thm.match (pat, concl)
+  val pat = Drule.strip_imp_concl (cprop_of thm)
+  val insts = Thm.match (pat, concl)
 in
- rtac (Drule.instantiate insts thm) 1
-end))
+  rtac (Drule.instantiate insts thm) 1
+end)
 *}