src/Pure/Isar/expression.ML
changeset 42381 309ec68442c6
parent 42375 774df7c59508
child 42440 5e7a7343ab11
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Apr 17 21:17:45 2011 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Apr 17 21:42:47 2011 +0200
     1.3 @@ -746,7 +746,7 @@
     1.4      val _ =
     1.5        if null extraTs then ()
     1.6        else warning ("Additional type variable(s) in locale specification " ^
     1.7 -        quote (Binding.str_of binding) ^ ": " ^
     1.8 +          Binding.print binding ^ ": " ^
     1.9            commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_wrt #1 extraTs)));
    1.10  
    1.11      val predicate_binding =