src/HOL/Tools/inductive_realizer.ML
changeset 26343 0dd2eab7b296
parent 26336 a0e2b706ce73
child 26477 ecf06644f6cb
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Mar 19 22:50:42 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 20 00:20:44 2008 +0100
     1.3 @@ -276,7 +276,7 @@
     1.4  fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
     1.5    let
     1.6      val qualifier = NameSpace.qualifier (name_of_thm induct);
     1.7 -    val inducts = PureThy.get_thms thy (Facts.Named (NameSpace.qualified qualifier "inducts", NONE));
     1.8 +    val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts");
     1.9      val iTs = term_tvars (prop_of (hd intrs));
    1.10      val ar = length vs + length iTs;
    1.11      val params = InductivePackage.params_of raw_induct;