# HG changeset patch
# User wenzelm
# Date 1220456850 -7200
# Node ID 9d121b171a0aaea93f5cf569a6c6d31d70af3069
# Parent  3f76ae637f71a66d87c2d9c3425b86e80bef7219
Sign.declare_const: Name.binding;

diff -r 3f76ae637f71 -r 9d121b171a0a doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Sep 03 12:11:28 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Sep 03 17:47:30 2008 +0200
@@ -317,7 +317,7 @@
   a theory by constant declararion and primitive definitions:
 
   \smallskip\begin{mldecls}
-  @{ML "Sign.declare_const: Properties.T -> bstring * typ * mixfix
+  @{ML "Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix
   -> theory -> term * theory"} \\
   @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
   \end{mldecls}
@@ -330,7 +330,7 @@
   @{ML "(fn (t, thy) => Thm.add_def false false
   (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
     (Sign.declare_const []
-      (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"}
+      ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
   \end{mldecls}
 
   \noindent With increasing numbers of applications, this code gets quite
@@ -344,7 +344,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
+|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |> (fn (t, thy) => thy
 |> Thm.add_def false false
      (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
@@ -368,7 +368,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
+|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |-> (fn t => Thm.add_def false false
       (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
 "}
@@ -378,7 +378,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
+|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
 |-> (fn def => Thm.add_def false false (\"bar_def\", def))
 "}
@@ -389,7 +389,7 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
+|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
 ||> Sign.add_path \"foobar\"
 |-> (fn t => Thm.add_def false false
       (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
@@ -401,8 +401,8 @@
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
-||>> Sign.declare_const [] (\"foobar\", @{typ \"foo => foo\"}, NoSyn)
+|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
+||>> Sign.declare_const [] ((Name.binding \"foobar\", @{typ \"foo => foo\"}), NoSyn)
 |-> (fn (t1, t2) => Thm.add_def false false
       (\"bar_def\", Logic.mk_equals (t1, t2)))
 "}
@@ -448,7 +448,7 @@
 in
   thy
   |> fold_map (fn const => Sign.declare_const []
-       (const, @{typ \"foo => foo\"}, NoSyn)) consts
+       ((Name.binding const, @{typ \"foo => foo\"}), NoSyn)) consts
   |>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
   |-> (fn defs => fold_map (fn def =>
        Thm.add_def false false (\"\", def)) defs)
@@ -486,12 +486,12 @@
   \smallskip\begin{mldecls}
 @{ML "thy
 |> tap (fn _ => writeln \"now adding constant\")
-|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
+|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
 ||>> `(fn thy => Sign.declared_const thy
          (Sign.full_name thy \"foobar\"))
 |-> (fn (t, b) => if b then I
        else Sign.declare_const []
-         (\"foobar\", @{typ \"foo => foo\"}, NoSyn) #> snd)
+         ((Name.binding \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
 "}
   \end{mldecls}
 *}
diff -r 3f76ae637f71 -r 9d121b171a0a doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Sep 03 12:11:28 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Sep 03 17:47:30 2008 +0200
@@ -369,7 +369,7 @@
   a theory by constant declararion and primitive definitions:
 
   \smallskip\begin{mldecls}
-  \verb|Sign.declare_const: Properties.T -> bstring * typ * mixfix|\isasep\isanewline%
+  \verb|Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix|\isasep\isanewline%
 \verb|  -> theory -> term * theory| \\
   \verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
   \end{mldecls}
@@ -382,7 +382,7 @@
   \verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
 \verb|  ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
 \verb|    (Sign.declare_const []|\isasep\isanewline%
-\verb|      ("bar", @{typ "foo => foo"}, NoSyn) thy)|
+\verb|      ((Name.binding "bar", @{typ "foo => foo"}), NoSyn) thy)|
   \end{mldecls}
 
   \noindent With increasing numbers of applications, this code gets quite
@@ -397,7 +397,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline%
 \verb|     ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
@@ -436,7 +436,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
 \verb|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
 
@@ -446,7 +446,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
 \verb||\verb,|,\verb|-> (fn def => Thm.add_def false false ("bar_def", def))|\isasep\isanewline%
 
@@ -457,7 +457,7 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
 \verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
 \verb|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
@@ -469,8 +469,8 @@
 
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ("foobar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Name.binding "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline%
 \verb|      ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
 
@@ -531,7 +531,7 @@
 \verb|in|\isasep\isanewline%
 \verb|  thy|\isasep\isanewline%
 \verb|  |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline%
-\verb|       (const, @{typ "foo => foo"}, NoSyn)) consts|\isasep\isanewline%
+\verb|       ((Name.binding const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline%
 \verb|  |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
 \verb|  |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline%
 \verb|       Thm.add_def false false ("", def)) defs)|\isasep\isanewline%
@@ -599,12 +599,12 @@
   \smallskip\begin{mldecls}
 \verb|thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline%
 \verb|         (Sign.full_name thy "foobar"))|\isasep\isanewline%
 \verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline%
 \verb|       else Sign.declare_const []|\isasep\isanewline%
-\verb|         ("foobar", @{typ "foo => foo"}, NoSyn) #> snd)|\isasep\isanewline%
+\verb|         ((Name.binding "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
 
   \end{mldecls}%
 \end{isamarkuptext}%
diff -r 3f76ae637f71 -r 9d121b171a0a doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Sep 03 12:11:28 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Sep 03 17:47:30 2008 +0200
@@ -328,7 +328,7 @@
   \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
   \indexml{lambda}\verb|lambda: term -> term -> term| \\
   \indexml{betapply}\verb|betapply: term * term -> term| \\
-  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> bstring * typ * mixfix ->|\isasep\isanewline%
+  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix ->|\isasep\isanewline%
 \verb|  theory -> term * theory| \\
   \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> bstring * term ->|\isasep\isanewline%
 \verb|  theory -> (term * term) * theory| \\
@@ -368,7 +368,7 @@
   \item \verb|betapply|~\isa{{\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion if \isa{t} is an
   abstraction.
 
-  \item \verb|Sign.declare_const|~\isa{properties\ {\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}}
+  \item \verb|Sign.declare_const|~\isa{properties\ {\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}}
   declares a new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix
   syntax.
 
diff -r 3f76ae637f71 -r 9d121b171a0a doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Wed Sep 03 12:11:28 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Wed Sep 03 17:47:30 2008 +0200
@@ -326,7 +326,7 @@
   @{index_ML fastype_of: "term -> typ"} \\
   @{index_ML lambda: "term -> term -> term"} \\
   @{index_ML betapply: "term * term -> term"} \\
-  @{index_ML Sign.declare_const: "Properties.T -> bstring * typ * mixfix ->
+  @{index_ML Sign.declare_const: "Properties.T -> (Name.binding * typ) * mixfix ->
   theory -> term * theory"} \\
   @{index_ML Sign.add_abbrev: "string -> Properties.T -> bstring * term ->
   theory -> (term * term) * theory"} \\
@@ -374,7 +374,7 @@
   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
   abstraction.
 
-  \item @{ML Sign.declare_const}~@{text "properties (c, \<sigma>, mx)"}
+  \item @{ML Sign.declare_const}~@{text "properties ((c, \<sigma>), mx)"}
   declares a new constant @{text "c :: \<sigma>"} with optional mixfix
   syntax.
 
diff -r 3f76ae637f71 -r 9d121b171a0a doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Sep 03 12:11:28 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Sep 03 17:47:30 2008 +0200
@@ -154,7 +154,7 @@
 %
 \begin{isamarkuptext}%
 \begin{matharray}{rcll}
-    \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
+    \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isarkeep{theory} & (axiomatic!)\\
     \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isarkeep{local{\dsh}theory} \\
     \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isaratt \\
     \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isarkeep{local{\dsh}theory} \\
@@ -194,8 +194,9 @@
   prevents additional specifications being issued later on.
   
   Note that axiomatic specifications are only appropriate when
-  declaring a new logical system.  Normal applications should only use
-  definitional mechanisms!
+  declaring a new logical system; axiomatic specifications are
+  restricted to global theory contexts.  Normal applications should
+  only use definitional mechanisms!
 
   \item [\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] produces an
   internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification
diff -r 3f76ae637f71 -r 9d121b171a0a src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Wed Sep 03 12:11:28 2008 +0200
+++ b/src/HOL/Library/Eval.thy	Wed Sep 03 17:47:30 2008 +0200
@@ -170,7 +170,7 @@
 end
 *}
 setup {*
-  Sign.declare_const [] ("rterm_of", @{typ "'a \<Rightarrow> 'b"}, NoSyn)
+  Sign.declare_const [] ((Name.binding "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
   #> snd
 *}
 
diff -r 3f76ae637f71 -r 9d121b171a0a src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Sep 03 12:11:28 2008 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Sep 03 17:47:30 2008 +0200
@@ -315,7 +315,7 @@
           val fns = (List.concat (Library.take (i, case_dummy_fns))) @
             fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
           val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
-          val decl = (Sign.base_name name, caseT, NoSyn);
+          val decl = ((Name.binding (Sign.base_name name), caseT), NoSyn);
           val def = ((Sign.base_name name) ^ "_def",
             Logic.mk_equals (list_comb (Const (name, caseT), fns1),
               list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
diff -r 3f76ae637f71 -r 9d121b171a0a src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Sep 03 12:11:28 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Wed Sep 03 17:47:30 2008 +0200
@@ -84,7 +84,8 @@
             val cT = extraTs ---> Ts ---> T
             val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
                     (*Forms a lambda-abstraction over the formal parameters*)
-            val (c, thy') = Sign.declare_const [Markup.property_internal] (cname, cT, NoSyn) thy
+            val (c, thy') =
+              Sign.declare_const [Markup.property_internal] ((Name.binding cname, cT), NoSyn) thy
             val cdef = cname ^ "_def"
             val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
             val ax = Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef)
diff -r 3f76ae637f71 -r 9d121b171a0a src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Sep 03 12:11:28 2008 +0200
+++ b/src/Pure/Isar/class.ML	Wed Sep 03 17:47:30 2008 +0200
@@ -496,7 +496,7 @@
     fun get_axiom thy = ((Thm.varifyT o Thm.get_axiom_i thy) c', thy);
   in
     thy'
-    |> Sign.declare_const pos (c, ty'', mx) |> snd
+    |> Sign.declare_const pos ((Name.binding c, ty''), mx) |> snd
     |> Thm.add_def false false (c, def_eq)
     |>> Thm.symmetric
     ||>> get_axiom
@@ -604,7 +604,7 @@
         val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v;
       in
         thy
-        |> Sign.declare_const [] (v, ty0, syn)
+        |> Sign.declare_const [] ((Name.binding v, ty0), syn)
         |> snd
         |> pair ((v, ty), (c, ty'))
       end;
diff -r 3f76ae637f71 -r 9d121b171a0a src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Sep 03 12:11:28 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Sep 03 17:47:30 2008 +0200
@@ -1781,7 +1781,7 @@
     val ([pred_def], defs_thy) =
       thy
       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
-      |> Sign.declare_const [] (bname, predT, NoSyn) |> snd
+      |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
       |> PureThy.add_defs false
         [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
diff -r 3f76ae637f71 -r 9d121b171a0a src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Sep 03 12:11:28 2008 +0200
+++ b/src/Pure/axclass.ML	Wed Sep 03 17:47:30 2008 +0200
@@ -370,7 +370,7 @@
     thy
     |> Sign.sticky_prefix name_inst
     |> Sign.no_base_names
-    |> Sign.declare_const [] (c', T', NoSyn)
+    |> Sign.declare_const [] ((Name.binding c', T'), NoSyn)
     |-> (fn const' as Const (c'', _) => Thm.add_def false true
           (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
     #>> Thm.varifyT