# 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) =