doc-src/IsarImplementation/Thy/ML.thy

   continued by an application of a function @{ML_text "g : foo -> bar"},
   and so on.  As a canoncial example, take functions enriching
   a theory by constant declararion and primitive definitions:
 
   \smallskip\begin{mldecls}
-  @{ML "Sign.declare_const: Properties.T -> (binding * typ) * mixfix
+  @{ML "Sign.declare_const: (binding * typ) * mixfix
   -> theory -> term * theory"} \\
   @{ML "Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory"}
   \end{mldecls}
 
   \noindent Written with naive application, an addition of constant

   a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
 
   \smallskip\begin{mldecls}
   @{ML "(fn (t, thy) => Thm.add_def false false
   (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
-    (Sign.declare_const []
+    (Sign.declare_const
       ((Binding.name \"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

   \noindent At this stage, Isabelle offers some combinators which allow
   for more convenient notation, most notably reverse application:
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |> (fn (t, thy) => thy
 |> Thm.add_def false false
      (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
   \end{mldecls}
 *}

   set of combinators is at hand, most notably @{ML "op |->"}
   which allows curried access to side results:
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |-> (fn t => Thm.add_def false false
       (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
 "}
   \end{mldecls}
 
   \noindent @{ML "op |>>"} allows for processing side results on their own:
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
 |-> (fn def => Thm.add_def false false (Binding.name \"bar_def\", def))
 "}
   \end{mldecls}
 
   \noindent Orthogonally, @{ML "op ||>"} applies a transformation
   in the presence of side results which are left unchanged:
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 ||> Sign.add_path \"foobar\"
 |-> (fn t => Thm.add_def false false
       (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
 ||> Sign.restore_naming thy
 "}

 
   \noindent @{ML "op ||>>"} accumulates side results:
 
   \smallskip\begin{mldecls}
 @{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
-||>> Sign.declare_const [] ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+||>> Sign.declare_const ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
 |-> (fn (t1, t2) => Thm.add_def false false
       (Binding.name \"bar_def\", Logic.mk_equals (t1, t2)))
 "}
   \end{mldecls}
 *}

   \smallskip\begin{mldecls}
 @{ML "let
   val consts = [\"foo\", \"bar\"];
 in
   thy
-  |> fold_map (fn const => Sign.declare_const []
+  |> fold_map (fn const => Sign.declare_const
        ((Binding.name 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 (Binding.empty, def)) defs)
 end"}

   in a series of context transformations:
 
   \smallskip\begin{mldecls}
 @{ML "thy
 |> tap (fn _ => writeln \"now adding constant\")
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 ||>> `(fn thy => Sign.declared_const thy
          (Sign.full_name thy (Binding.name \"foobar\")))
 |-> (fn (t, b) => if b then I
-       else Sign.declare_const []
+       else Sign.declare_const
          ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
 "}
   \end{mldecls}
 *}