--- a/src/HOL/Tools/inductive_realizer.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Mar 19 22:27:57 2008 +0100
@@ -276,8 +276,7 @@
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 (Name
- (NameSpace.qualified qualifier "inducts"));
+ val inducts = PureThy.get_thms thy (Facts.Named (NameSpace.qualified qualifier "inducts", NONE));
val iTs = term_tvars (prop_of (hd intrs));
val ar = length vs + length iTs;
val params = InductivePackage.params_of raw_induct;