src/HOL/Tools/datatype_package.ML

       (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
         atac 2, resolve_tac thms 1, etac FalseE 1]))
   | ManyConstrs (thm, simpset) =>
       let
         val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
-          map (fn a => get_thm (ThyInfo.the_theory "Datatype" thy) (Facts.Named (a, NONE)))
+          map (PureThy.get_thm (ThyInfo.the_theory "Datatype" thy))
             ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
       in
         Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
         (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
           full_simp_tac (Simplifier.inherit_context ss simpset) 1,