# HG changeset patch
# User wenzelm
# Date 1275653756 -7200
# Node ID 715d25555ca6817a1abcec7eb7039726b90062dc
# Parent  664d3110beb2da56e8ca6b34f03f56e738bd6436
tuned warning;

diff -r 664d3110beb2 -r 715d25555ca6 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Jun 04 11:31:33 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Jun 04 14:15:56 2010 +0200
@@ -732,18 +732,20 @@
       prep_decl raw_import I raw_body (ProofContext.init_global thy);
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
 
+    val extraTs =
+      subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
+    val _ =
+      if null extraTs then ()
+      else warning ("Additional type variable(s) in locale specification " ^
+        quote (Binding.str_of binding) ^ ": " ^
+          commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_wrt #1 extraTs)));
+
     val predicate_binding =
       if Binding.is_empty raw_predicate_binding then binding
       else raw_predicate_binding;
     val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
       define_preds predicate_binding parms text thy;
 
-    val extraTs = subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
-    val _ =
-      if null extraTs then ()
-      else warning ("Additional type variable(s) in locale specification " ^
-        quote (Binding.str_of binding));
-
     val a_satisfy = Element.satisfy_morphism a_axioms;
     val b_satisfy = Element.satisfy_morphism b_axioms;