--- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Mon Nov 10 21:49:48 2014 +0100
@@ -80,7 +80,7 @@
TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
TRY (simp_tac simpset3 1), TRY (simp_tac (put_simpset cooper_ss ctxt) 1)]
(Thm.trivial ct))
- fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
+ fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i)
(* The result of the quantifier elimination *)
val (th, tac) =
(case (prop_of pre_thm) of