src/HOL/Tools/inductive_package.ML

   fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2),
     Library.generic_merge Thm.eq_thm I I monos1 monos2);
 
   fun print sg (tab, monos) =
     [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
-     Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)]
+     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
     |> Pretty.chunks |> Pretty.writeln;
 end;
 
 structure InductiveData = TheoryDataFun(InductiveArgs);
 val print_inductives = InductiveData.print;