src/HOL/Tools/inductive_realizer.ML

 fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
 
 fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
   let
     val qualifier = NameSpace.qualifier (name_of_thm induct);
-    val inducts = PureThy.get_thms thy (Facts.Named (NameSpace.qualified qualifier "inducts", NONE));
+    val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts");
     val iTs = term_tvars (prop_of (hd intrs));
     val ar = length vs + length iTs;
     val params = InductivePackage.params_of raw_induct;
     val arities = InductivePackage.arities_of raw_induct;
     val nparms = length params;