diff -r 0b6217fda81b -r abe08fb15a12 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -319,7 +319,7 @@
       if ! Ind_Syntax.trace then
         writeln (cat_lines
           (["ind_prems:"] @ map (Syntax.string_of_term ctxt1) ind_prems @
-           ["raw_induct:", Display.string_of_thm ctxt1 raw_induct]))
+           ["raw_induct:", Thm.string_of_thm ctxt1 raw_induct]))
       else ();
 
 
@@ -352,7 +352,7 @@
 
      val dummy =
       if ! Ind_Syntax.trace then
-        writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct)
+        writeln ("quant_induct:\n" ^ Thm.string_of_thm ctxt1 quant_induct)
       else ();
 
 
@@ -429,7 +429,7 @@
 
      val dummy =
       if ! Ind_Syntax.trace then
-        writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma)
+        writeln ("lemma: " ^ Thm.string_of_thm ctxt1 lemma)
       else ();