src/Tools/induct.ML

     val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
     val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal));
   in
     if not (null params) then
       (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
-        commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_boundT) params));
+        commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_bound_abs) params));
       Seq.single rule)
     else
       let
         val rule' = Thm.incr_indexes (maxidx + 1) rule;
         val concl = Logic.strip_assums_concl goal;