src/Pure/Isar/locale.ML

     string option * (cterm list * cterm list) * context * context *
       (term * (term list * term list)) list list
 
   (* Diagnostic functions *)
   val print_locales: theory -> unit
-  val print_locale: theory -> expr -> element list -> unit
+  val print_locale: theory -> bool -> expr -> element list -> unit
   val print_global_registrations: bool -> string -> theory -> unit
   val print_local_registrations': bool -> string -> context -> unit
   val print_local_registrations: bool -> string -> context -> unit
 
   (* Storing results *)

 
 (** define locales **)
 
 (* print locale *)
 
-fun print_locale thy import body =
+fun print_locale thy show_facts import body =
   let
     val thy_ctxt = ProofContext.init thy;
     val (((_, import_elemss), (ctxt, elemss, _)), _) = read_context import body thy_ctxt;
     val all_elems = List.concat (map #2 (import_elemss @ elemss));
 

       | items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items "  and" xs;
     fun prt_elem (Fixes fixes) = items "fixes" (map prt_fix fixes)
       | prt_elem (Constrains csts) = items "constrains" (map prt_cst csts)
       | prt_elem (Assumes asms) = items "assumes" (map prt_asm asms)
       | prt_elem (Defines defs) = items "defines" (map prt_def defs)
-      | prt_elem (Notes facts) = items "notes" (map prt_note facts);
+      | prt_elem (Notes facts) =
+        if show_facts then items "notes" (map prt_note facts) else [];
   in
     Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems)
     |> Pretty.writeln
   end;
 

     val name = Sign.full_name thy bname;
     val _ = conditional (isSome (get_locale thy name)) (fn () =>
       error ("Duplicate definition of locale " ^ quote name));
 
     val thy_ctxt = ProofContext.init thy;
-    val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), text) =
+    val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
+      text as (parms, ((_, exts'), _), _)) =
       prep_ctxt raw_import raw_body thy_ctxt;
     val elemss = import_elemss @ body_elemss;
     val import = prep_expr thy raw_import;
+
+    val extraTs = foldr Term.add_term_tfrees [] exts' \\
+      foldr Term.add_typ_tfrees [] (map #2 parms);
+    val _ = if null extraTs then ()
+      else warning ("Encountered type variables in specification text that don't occur in the\n" ^ "locale parameters.");        
 
     val (pred_thy, (elemss', predicate as (predicate_statement, predicate_axioms))) =
       if do_pred then thy |> define_preds bname text elemss
       else (thy, (elemss, ([], [])));
     val pred_ctxt = ProofContext.init pred_thy;