doc-src/IsarImplementation/Thy/document/ML.tex

   continued by an application of a function \verb|g : foo -> bar|,
   and so on.  As a canoncial example, take functions enriching
   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}
 
   \noindent Written with naive application, an addition of constant

 
   \smallskip\begin{mldecls}
   \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
   unreadable.  Further, it is unintuitive that things are
   written down in the opposite order as they actually ``happen''.%

 \noindent At this stage, Isabelle offers some combinators which allow
   for more convenient notation, most notably reverse application:
 
   \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"})))|
   \end{mldecls}%
 \end{isamarkuptext}%

   set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->|
   which allows curried access to side results:
 
   \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%
 
   \end{mldecls}
 
   \noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own:
 
   \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%
 
   \end{mldecls}
 
   \noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation
   in the presence of side results which are left unchanged:
 
   \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%
 \verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline%
 

 
   \noindent \verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results:
 
   \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%
 
   \end{mldecls}%
 \end{isamarkuptext}%

 \verb|let|\isasep\isanewline%
 \verb|  val consts = ["foo", "bar"];|\isasep\isanewline%
 \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%
 \verb|end|
   \end{mldecls}%

   in a series of context transformations:
 
   \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}%
 \isamarkuptrue%
 %