src/HOL/Tools/SMT/verit_replay.ML

 
     (*for sko_ex and sko_forall, assumptions are in proofs',  but the definition of the skolem
        function is in proofs *)
     val nthms = prems
       |> map (apsnd export_thm) o map_filter (Symtab.lookup (if (null subproof) then proofs else proofs'))
-    val nthms' = (if Verit_Proof.is_skolemisation rule
+    val nthms' = (if Verit_Proof.is_skolemization rule
          then prems else [])
       |> map_filter (Symtab.lookup proofs)
     val args = map (Term.subst_free concl_tranformation o subst_only_free global_transformation) args
     val insts = Symtab.map (K (Term.subst_free concl_tranformation o subst_only_free global_transformation)) insts
     val proof_prems =