src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML

     val ((_, intros), ctxt') = Variable.import true intros ctxt
     val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
       (flatten constname) (map prop_of intros) ([], thy)
     val ctxt'' = Proof_Context.transfer thy' ctxt'
     val intros'' =
-      map (fn t => Goal.prove ctxt'' [] [] t (fn _ => ALLGOALS Skip_Proof.cheat_tac)) intros'
+      map (fn t => Goal.prove ctxt'' [] [] t (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt''))) intros'
       |> Variable.export ctxt'' ctxt
   in
     (intros'', (local_defs, thy'))
   end