src/HOL/Tools/recdef_package.ML

         mk_hints (Drule.merge_rules (simps1, simps2),
           Library.merge_alists congs1 congs2,
           Drule.merge_rules (wfs1, wfs2)));
 
   fun print sg (tab, hints) =
-   (Pretty.strs ("recdefs:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)) ::
+   (Pretty.strs ("recdefs:" :: map #1 (Sign.extern_table sg Sign.constK tab)) ::
      pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
 end;
 
 structure GlobalRecdefData = TheoryDataFun(GlobalRecdefArgs);
 val print_recdefs = GlobalRecdefData.print;