diff -r e3eb88d79ad7 -r c10e314761fa QuotMain.thy
--- a/QuotMain.thy	Fri Nov 27 02:58:28 2009 +0100
+++ b/QuotMain.thy	Fri Nov 27 03:33:30 2009 +0100
@@ -1042,29 +1042,27 @@
 
 ML {*
 fun inst_spec ctrm =
-let
-   val cty = ctyp_of_term ctrm
-in
-   Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}
-end
+   Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
 
 fun inst_spec_tac ctrms =
   EVERY' (map (dtac o inst_spec) ctrms)
 
-fun abs_list (xs, t) = 
-  fold (fn (x, T) => fn t' => HOLogic.all_const T $ (lambda (Free (x, T)) t')) xs t
+fun abs_list xs trm = 
+  fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
+
+fun apply_under_Trueprop f = 
+  HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
 
 fun gen_frees_tac ctxt =
  SUBGOAL (fn (concl, i) =>
   let
     val thy = ProofContext.theory_of ctxt
-    val concl' = HOLogic.dest_Trueprop concl
-    val vrs = Term.add_frees concl' []
+    val vrs = Term.add_frees concl []
     val cvrs = map (cterm_of thy o Free) vrs
-    val concl'' = HOLogic.mk_Trueprop (abs_list (vrs, concl'))
-    val goal = Logic.mk_implies (concl'', concl)
+    val concl' = apply_under_Trueprop (abs_list vrs) concl
+    val goal = Logic.mk_implies (concl', concl)
     val rule = Goal.prove ctxt [] [] goal 
-      (K ((inst_spec_tac (rev cvrs) THEN' atac) 1))
+      (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
   in
     rtac rule i
   end)