1.1 --- a/src/Pure/Isar/expression.ML	Fri Jun 04 11:31:33 2010 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Jun 04 14:15:56 2010 +0200
     1.3 @@ -732,18 +732,20 @@
     1.4        prep_decl raw_import I raw_body (ProofContext.init_global thy);
     1.5      val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
     1.6  
     1.7 +    val extraTs =
     1.8 +      subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
     1.9 +    val _ =
    1.10 +      if null extraTs then ()
    1.11 +      else warning ("Additional type variable(s) in locale specification " ^
    1.12 +        quote (Binding.str_of binding) ^ ": " ^
    1.13 +          commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_wrt #1 extraTs)));
    1.14 +
    1.15      val predicate_binding =
    1.16        if Binding.is_empty raw_predicate_binding then binding
    1.17        else raw_predicate_binding;
    1.18      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
    1.19        define_preds predicate_binding parms text thy;
    1.20  
    1.21 -    val extraTs = subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
    1.22 -    val _ =
    1.23 -      if null extraTs then ()
    1.24 -      else warning ("Additional type variable(s) in locale specification " ^
    1.25 -        quote (Binding.str_of binding));
    1.26 -
    1.27      val a_satisfy = Element.satisfy_morphism a_axioms;
    1.28      val b_satisfy = Element.satisfy_morphism b_axioms;
    1.29