src/HOL/SPARK/Tools/spark_vcs.ML

       (HOLogic.mk_Trueprop (HOLogic.mk_eq
          (HOLogic.mk_UNIV T, HOLogic.mk_set T cs)))
       (fn _ =>
          rtac @{thm subset_antisym} 1 THEN
          rtac @{thm subsetI} 1 THEN
-         Old_Datatype_Aux.exh_tac (K (#exhaust (BNF_LFP_Compat.the_info
+         Old_Datatype_Aux.exh_tac lthy (K (#exhaust (BNF_LFP_Compat.the_info
            (Proof_Context.theory_of lthy) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
          ALLGOALS (asm_full_simp_tac lthy));
 
     val finite_UNIV = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (Const (@{const_name finite},