src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy

 ML {* 
 structure Parametric_Ferrante_Rackoff = 
 struct
 
 fun tactic ctxt alternative T ps = 
-  Object_Logic.full_atomize_tac
+  Object_Logic.full_atomize_tac ctxt
   THEN' CSUBGOAL (fn (g, i) =>
     let
       val th = frpar_oracle (ctxt, alternative, T, ps, g)
     in rtac (th RS iffD2) i end);