doc-src/IsarImplementation/Thy/ML.thy

   a theory by constant declararion and primitive definitions:
 
   \smallskip\begin{mldecls}
   @{ML "Sign.declare_const: Properties.T -> (binding * typ) * mixfix
   -> theory -> term * theory"} \\
-  @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
+  @{ML "Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory"}
   \end{mldecls}
 
   \noindent Written with naive application, an addition of constant
   @{term bar} with type @{typ "foo \<Rightarrow> foo"} and
   a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
 
   \smallskip\begin{mldecls}
   @{ML "(fn (t, thy) => Thm.add_def false false
-  (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
+  (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
     (Sign.declare_const []
       ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
   \end{mldecls}
 
   \noindent With increasing numbers of applications, this code gets quite

   \smallskip\begin{mldecls}
 @{ML "thy
 |> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |> (fn (t, thy) => thy
 |> Thm.add_def false false
-     (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
+     (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
   \end{mldecls}
 *}
 
 text %mlref {*
   \begin{mldecls}

 
   \smallskip\begin{mldecls}
 @{ML "thy
 |> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |-> (fn t => Thm.add_def false false
-      (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
+      (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)
 |>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
-|-> (fn def => Thm.add_def false false (\"bar_def\", def))
+|-> (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.add_path \"foobar\"
 |-> (fn t => Thm.add_def false false
-      (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
+      (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
 ||> Sign.restore_naming thy
 "}
   \end{mldecls}
 
   \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)
 |-> (fn (t1, t2) => Thm.add_def false false
-      (\"bar_def\", Logic.mk_equals (t1, t2)))
+      (Binding.name \"bar_def\", Logic.mk_equals (t1, t2)))
 "}
   \end{mldecls}
 *}
 
 text %mlref {*

   thy
   |> 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 (\"\", def)) defs)
+       Thm.add_def false false (Binding.empty, def)) defs)
 end"}
   \end{mldecls}
 *}
 
 text %mlref {*