src/HOL/Tools/induct_method.ML

 val type_rules = NetRules.init eq_rule (Thm.concl_of o #2);
 val set_rules = NetRules.init eq_rule (Thm.major_prem_of o #2);
 
 fun lookup_rule (rs:rules) name = Library.assoc (NetRules.rules rs, name);
 
-fun print_rules kind rs =
+fun print_rules kind sg rs =
   let val thms = map snd (NetRules.rules rs)
-  in Pretty.writeln (Pretty.big_list kind (map Display.pretty_thm thms)) end;
+  in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end;
 
 
 (* theory data kind 'HOL/induct_method' *)
 
 structure GlobalInductArgs =

   fun merge (((casesT1, casesS1), (inductT1, inductS1)),
       ((casesT2, casesS2), (inductT2, inductS2))) =
     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
 
-  fun print _ ((casesT, casesS), (inductT, inductS)) =
-    (print_rules "type cases:" casesT;
-      print_rules "set cases:" casesS;
-      print_rules "type induct:" inductT;
-      print_rules "set induct:" inductS);
+  fun print sg ((casesT, casesS), (inductT, inductS)) =
+    (print_rules "type cases:" sg casesT;
+      print_rules "set cases:" sg casesS;
+      print_rules "type induct:" sg inductT;
+      print_rules "set induct:" sg inductS);
 
   fun dest ((casesT, casesS), (inductT, inductS)) =
     {type_cases = NetRules.rules casesT,
      set_cases = NetRules.rules casesS,
      type_induct = NetRules.rules inductT,

 struct
   val name = "HOL/induct_method";
   type T = GlobalInductArgs.T;
 
   fun init thy = GlobalInduct.get thy;
-  fun print x = GlobalInductArgs.print x;
+  val print = GlobalInductArgs.print o ProofContext.sign_of;
 end;
 
 structure LocalInduct = ProofDataFun(LocalInductArgs);
 val print_local_rules = LocalInduct.print;
 val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;