# HG changeset patch # User haftmann # Date 1232611485 -3600 # Node ID 4f68e0f8f4fd8c988e8fc4e40da17d90c86a474f # Parent 9891e3646809346aa1f78074214c843a893f631c binding replaces bstring diff -r 9891e3646809 -r 4f68e0f8f4fd doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Wed Jan 21 23:42:37 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Jan 22 09:04:45 2009 +0100 @@ -319,7 +319,7 @@ \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 @@ -328,7 +328,7 @@ \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} @@ -347,7 +347,7 @@ |> 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} *} @@ -370,7 +370,7 @@ @{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} @@ -380,7 +380,7 @@ @{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} @@ -392,7 +392,7 @@ |> 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} @@ -404,7 +404,7 @@ |> 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} *} @@ -451,7 +451,7 @@ ((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} *} diff -r 9891e3646809 -r 4f68e0f8f4fd doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 21 23:42:37 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Jan 22 09:04:45 2009 +0100 @@ -368,7 +368,7 @@ \smallskip\begin{mldecls} \verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline% \verb| -> theory -> term * theory| \\ - \verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory| + \verb|Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory| \end{mldecls} \noindent Written with naive application, an addition of constant @@ -377,7 +377,7 @@ \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| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline% \verb| (Sign.declare_const []|\isasep\isanewline% \verb| ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)| \end{mldecls} @@ -397,7 +397,7 @@ \verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "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"})))| +\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))| \end{mldecls}% \end{isamarkuptext}% \isamarkuptrue% @@ -435,7 +435,7 @@ \verb|thy|\isasep\isanewline% \verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "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% +\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline% \end{mldecls} @@ -445,7 +445,7 @@ \verb|thy|\isasep\isanewline% \verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "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% +\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false (Binding.name "bar_def", def))|\isasep\isanewline% \end{mldecls} @@ -457,7 +457,7 @@ \verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "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| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline% \verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline% \end{mldecls} @@ -469,7 +469,7 @@ \verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% \verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Binding.name "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% +\verb| (Binding.name "bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline% \end{mldecls}% \end{isamarkuptext}% @@ -531,7 +531,7 @@ \verb| ((Binding.name 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| Thm.add_def false false (Binding.empty, def)) defs)|\isasep\isanewline% \verb|end| \end{mldecls}% \end{isamarkuptext}%