# HG changeset patch
# User wenzelm
# Date 1442954568 -7200
# Node ID 9ce5de06cd3b0a6f07d1e183e9d8c768138da352
# Parent  15865e0c55985ddef2fc885bcdca2d7c0d9a7571
tuned signature;

diff -r 15865e0c5598 -r 9ce5de06cd3b src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Sep 22 22:38:22 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Sep 22 22:42:48 2015 +0200
@@ -85,7 +85,7 @@
 
     val const_space = Proof_Context.const_space ctxt;
     val type_space = Proof_Context.type_space ctxt;
-    val item_space = fn Defs.Constant => const_space | Defs.Type => type_space;
+    val item_space = fn Defs.Const => const_space | Defs.Type => type_space;
     fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
 
     fun markup_extern_item (kind, name) =
diff -r 15865e0c5598 -r 9ce5de06cd3b src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Sep 22 22:38:22 2015 +0200
+++ b/src/Pure/axclass.ML	Tue Sep 22 22:42:48 2015 +0200
@@ -597,7 +597,7 @@
   (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
 
 fun class_const_dep c =
-  ((Defs.Constant, Logic.const_of_class c), [Term.aT []]);
+  ((Defs.Const, Logic.const_of_class c), [Term.aT []]);
 
 in
 
diff -r 15865e0c5598 -r 9ce5de06cd3b src/Pure/defs.ML
--- a/src/Pure/defs.ML	Tue Sep 22 22:38:22 2015 +0200
+++ b/src/Pure/defs.ML	Tue Sep 22 22:42:48 2015 +0200
@@ -7,7 +7,7 @@
 
 signature DEFS =
 sig
-  datatype item_kind = Constant | Type
+  datatype item_kind = Const | Type
   type item = item_kind * string
   val item_ord: item * item -> order
   type entry = item * typ list
@@ -35,17 +35,17 @@
 
 (* specification items *)
 
-datatype item_kind = Constant | Type;
+datatype item_kind = Const | Type;
 type item = item_kind * string;
 
-fun item_kind_ord (Constant, Type) = LESS
-  | item_kind_ord (Type, Constant) = GREATER
+fun item_kind_ord (Const, Type) = LESS
+  | item_kind_ord (Type, Const) = GREATER
   | item_kind_ord _ = EQUAL;
 
 val item_ord = prod_ord item_kind_ord string_ord;
 val fast_item_ord = prod_ord item_kind_ord fast_string_ord;
 
-fun print_item (k, s) = if k = Constant then s else "type " ^ s;
+fun print_item (k, s) = if k = Const then s else "type " ^ s;
 
 structure Itemtab = Table(type key = item val ord = fast_item_ord);
 
diff -r 15865e0c5598 -r 9ce5de06cd3b src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Sep 22 22:38:22 2015 +0200
+++ b/src/Pure/pure_thy.ML	Tue Sep 22 22:42:48 2015 +0200
@@ -198,11 +198,11 @@
     (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
     (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
     (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]
-  #> Theory.add_deps_global "Pure.eq" ((Defs.Constant, "Pure.eq"), [typ "'a"]) []
-  #> Theory.add_deps_global "Pure.imp" ((Defs.Constant, "Pure.imp"), []) []
-  #> Theory.add_deps_global "Pure.all" ((Defs.Constant, "Pure.all"), [typ "'a"]) []
-  #> Theory.add_deps_global "Pure.type" ((Defs.Constant, "Pure.type"), [typ "'a"]) []
-  #> Theory.add_deps_global "Pure.dummy_pattern" ((Defs.Constant, "Pure.dummy_pattern"), [typ "'a"]) []
+  #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) []
+  #> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) []
+  #> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) []
+  #> Theory.add_deps_global "Pure.type" ((Defs.Const, "Pure.type"), [typ "'a"]) []
+  #> Theory.add_deps_global "Pure.dummy_pattern" ((Defs.Const, "Pure.dummy_pattern"), [typ "'a"]) []
   #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
diff -r 15865e0c5598 -r 9ce5de06cd3b src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Sep 22 22:38:22 2015 +0200
+++ b/src/Pure/theory.ML	Tue Sep 22 22:42:48 2015 +0200
@@ -213,7 +213,7 @@
 
 (* dependencies *)
 
-fun const_dep thy (c, T) = ((Defs.Constant, c), Sign.const_typargs thy (c, T));
+fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T));
 fun type_dep (c, args) = ((Defs.Type, c), args);
 
 fun dependencies ctxt unchecked def description lhs rhs =
@@ -237,7 +237,7 @@
         "\nThe error(s) above occurred in " ^ quote description);
   in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end;
 
-fun cert_entry thy ((Defs.Constant, c), args) =
+fun cert_entry thy ((Defs.Const, c), args) =
       Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args)))
       |> dest_Const |> const_dep thy
   | cert_entry thy ((Defs.Type, c), args) =