# HG changeset patch
# User wenzelm
# Date 1452770449 -3600
# Node ID e089e5b02443bccb3b7d0e91a5f19f262bb02944
# Parent  c3c98ed94b0f7c738e65e66f9bdefaced354bae3
tuned;

diff -r c3c98ed94b0f -r e089e5b02443 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Thu Jan 14 12:11:22 2016 +0100
+++ b/src/Pure/defs.ML	Thu Jan 14 12:20:49 2016 +0100
@@ -1,8 +1,9 @@
 (*  Title:      Pure/defs.ML
     Author:     Makarius
 
-Global well-formedness checks for constant definitions.  Covers plain
-definitions and simple sub-structural overloading.
+Global well-formedness checks for overloaded definitions (mixed constants and
+types). Recall that constant definitions may be explained syntactically within
+Pure, but type definitions require particular set-theoretic semantics.
 *)
 
 signature DEFS =
@@ -54,12 +55,12 @@
 
 (* pretty printing *)
 
-type context = Proof.context * (Name_Space.T * Name_Space.T)
+type context = Proof.context * (Name_Space.T * Name_Space.T);
 
 fun global_context thy =
   (Syntax.init_pretty_global thy, (Sign.const_space thy, Sign.type_space thy));
 
-fun space ((ctxt, spaces): context) kind =
+fun space ((_, spaces): context) kind =
   if kind = Const then #1 spaces else #2 spaces;
 
 fun pretty_item (context as (ctxt, _)) (kind, name) =