src/Tools/induct.ML
changeset 49660 de49d9b4d7bc
parent 47060 e2741ec9ae36
child 49748 a346daa8a1f4
     1.1 --- a/src/Tools/induct.ML	Sat Sep 29 16:51:04 2012 +0200
     1.2 +++ b/src/Tools/induct.ML	Sat Sep 29 18:23:46 2012 +0200
     1.3 @@ -597,7 +597,7 @@
     1.4    in
     1.5      if not (null params) then
     1.6        (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
     1.7 -        commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_boundT) params));
     1.8 +        commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_bound_abs) params));
     1.9        Seq.single rule)
    1.10      else
    1.11        let