--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Dec 13 23:53:02 2013 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sat Dec 14 17:28:05 2013 +0100
@@ -224,7 +224,7 @@
(case dlo_instance ctxt p of
NONE => no_tac
| SOME instance =>
- Object_Logic.full_atomize_tac i THEN
+ Object_Logic.full_atomize_tac ctxt i THEN
simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN (* FIXME already part of raw_ferrack_qe_conv? *)
CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
simp_tac ctxt i)); (* FIXME really? *)