# HG changeset patch
# User wenzelm
# Date 1377253851 -7200
# Node ID 7c2b13a53d697b4a870ee91d8649e5f329de5075
# Parent  f03ec7fae947c27a1f22b6df422da6024601d0ee
removed unused ML antiquotations @{let}, @{note};

diff -r f03ec7fae947 -r 7c2b13a53d69 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Fri Aug 23 11:44:28 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Fri Aug 23 12:30:51 2013 +0200
@@ -682,61 +682,6 @@
   scheme allows to refer to formal entities in a robust manner, with
   proper static scoping and with some degree of logical checking of
   small portions of the code.
-
-  Special antiquotations like @{text "@{let \<dots>}"} or @{text "@{note
-  \<dots>}"} augment the compilation context without generating code.  The
-  non-ASCII braces @{text "\<lbrace>"} and @{text "\<rbrace>"} allow to delimit the
-  effect by introducing local blocks within the pre-compilation
-  environment.
-
-  \medskip See also \cite{Wenzel-Chaieb:2007b} for a broader
-  perspective on Isabelle/ML antiquotations.  *}
-
-text %mlantiq {*
-  \begin{matharray}{rcl}
-  @{ML_antiquotation_def "let"} & : & @{text ML_antiquotation} \\
-  @{ML_antiquotation_def "note"} & : & @{text ML_antiquotation} \\
-  \end{matharray}
-
-  @{rail "
-  @@{ML_antiquotation let} ((term + @'and') '=' term + @'and')
-  ;
-  @@{ML_antiquotation note} (thmdef? thmrefs + @'and')
-  "}
-
-  \begin{description}
-
-  \item @{text "@{let p = t}"} binds schematic variables in the
-  pattern @{text "p"} by higher-order matching against the term @{text
-  "t"}.  This is analogous to the regular @{command_ref let} command
-  in the Isar proof language.  The pre-compilation environment is
-  augmented by auxiliary term bindings, without emitting ML source.
-
-  \item @{text "@{note a = b\<^sub>1 \<dots> b\<^sub>n}"} recalls existing facts @{text
-  "b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}.  This is analogous to
-  the regular @{command_ref note} command in the Isar proof language.
-  The pre-compilation environment is augmented by auxiliary fact
-  bindings, without emitting ML source.
-
-  \end{description}
-*}
-
-text %mlex {* The following artificial example gives some impression
-  about the antiquotation elements introduced so far, together with
-  the important @{text "@{thm}"} antiquotation defined later.
-*}
-
-ML {*
-  \<lbrace>
-    @{let ?t = my_term}
-    @{note my_refl = reflexive [of ?t]}
-    fun foo th = Thm.transitive th @{thm my_refl}
-  \<rbrace>
-*}
-
-text {* The extra block delimiters do not affect the compiled code
-  itself, i.e.\ function @{ML foo} is available in the present context
-  of this paragraph.
 *}
 
 
diff -r f03ec7fae947 -r 7c2b13a53d69 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Fri Aug 23 11:44:28 2013 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Fri Aug 23 12:30:51 2013 +0200
@@ -92,18 +92,6 @@
   inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
   inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
 
-  macro (Binding.name "let")
-    (Args.context --
-      Scan.lift
-        (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
-        >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))) #>
-
-  macro (Binding.name "note")
-    (Args.context :|-- (fn ctxt =>
-      Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms
-        >> (fn ((a, srcs), ths) => ((a, map (Attrib.attribute_cmd ctxt) srcs), [(ths, [])])))
-      >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #>
-
   value (Binding.name "ctyp") (Args.typ >> (fn T =>
     "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
       ML_Syntax.atomic (ML_Syntax.print_typ T))) #>