src/ZF/Tools/inductive_package.ML

   val intrs =
     (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
     |> ListPair.map (fn (t, tacs) =>
       Goal.prove_global thy1 [] [] t
         (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
-    handle MetaSimplifier.SIMPLIFIER (msg, thm) => (print_thm thm; error msg);
+    handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
 
   (********)
   val dummy = writeln "  Proving the elimination rule...";
 
   (*Breaks down logical connectives in the monotonic function*)

                          intr_tms;
 
      val dummy = if !Ind_Syntax.trace then
                  (writeln "ind_prems = ";
                   List.app (writeln o Syntax.string_of_term ctxt1) ind_prems;
-                  writeln "raw_induct = "; print_thm raw_induct)
+                  writeln "raw_induct = "; Display.print_thm raw_induct)
              else ();
 
 
      (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
        If the premises get simplified, then the proofs could fail.*)

             REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm exE}, @{thm conjE}]
                                ORELSE' bound_hyp_subst_tac)),
             ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
 
      val dummy = if !Ind_Syntax.trace then
-                 (writeln "quant_induct = "; print_thm quant_induct)
+                 (writeln "quant_induct = "; Display.print_thm quant_induct)
              else ();
 
 
      (*** Prove the simultaneous induction rule ***)
 

                [rewrite_goals_tac part_rec_defs,
                 REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
        else (writeln "  [ No mutual induction rule needed ]"; @{thm TrueI});
 
      val dummy = if !Ind_Syntax.trace then
-                 (writeln "lemma = "; print_thm lemma)
+                 (writeln "lemma = "; Display.print_thm lemma)
              else ();
 
 
      (*Mutual induction follows by freeness of Inl/Inr.*)