
diff -r 6103b0eadbf2 -r f7c97e64cc2a ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Advanced.thy	Thu May 16 19:56:12 2019 +0200
@@ -59,7 +59,7 @@
 
   Functions acting on theories often end with the suffix \<open>_global\<close>,
   for example the function @{ML read_term_global in Syntax} in the structure
-  @{ML_struct Syntax}. The reason is to set them syntactically apart from
+  @{ML_structure Syntax}. The reason is to set them syntactically apart from
   functions acting on contexts or local theories, which will be discussed in
   the next sections. There is a tendency amongst Isabelle developers to prefer
   ``non-global'' operations, because they have some advantages, as we will also
@@ -74,7 +74,7 @@
   the theory where the attribute has been registered or the theorem has been
   stored.  This is a fundamental principle in Isabelle. A similar situation
   arises with declaring a constant, which can be done on the ML-level with 
-  function @{ML_ind declare_const in Sign} from the structure @{ML_struct
+  function @{ML_ind declare_const in Sign} from the structure @{ML_structure
   Sign}. To see how \isacommand{setup} works, consider the following code:
 
 \<close>  
@@ -176,7 +176,7 @@
   the variables are fixed. For this remember that ML-code inside a proof
   needs to be enclosed inside \isacommand{ML\_prf}~\<open>\<verbopen> \<dots> \<verbclose>\<close>,
   not \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close>. The function 
-  @{ML_ind dest_fixes in Variable} from the structure @{ML_struct Variable} takes 
+  @{ML_ind dest_fixes in Variable} from the structure @{ML_structure Variable} takes 
   a context and returns all its currently fixed variable (names). That 
   means a context has a dataslot containing information about fixed variables.
   The ML-antiquotation \<open>@{context}\<close> points to the context that is
@@ -252,16 +252,16 @@
   of fixed variables is actually quite useful. For example it prevents us from 
   fixing a variable twice
 
-  @{ML_response_fake [gray, display]
+  @{ML_matchresult_fake [gray, display]
   "@{context}
 |> Variable.add_fixes [\"x\", \"x\"]" 
   "ERROR: Duplicate fixed variable(s): \"x\""}
 
   More importantly it also allows us to easily create fresh names for
   fixed variables.  For this you have to use the function @{ML_ind
-  variant_fixes in Variable} from the structure @{ML_struct Variable}.
+  variant_fixes in Variable} from the structure @{ML_structure Variable}.
 
-  @{ML_response_fake [gray, display]
+  @{ML_matchresult_fake [gray, display]
   "@{context}
 |> Variable.variant_fixes [\"y\", \"y\", \"z\"]" 
   "([\"y\", \"ya\", \"z\"], ...)"}
@@ -273,7 +273,7 @@
   create two fresh variables of type @{typ nat} as variants of the
   string @{text [quotes] "x"} (Lines 6 and 7).
 
-  @{ML_response_fake [display, gray, linenos]
+  @{ML_matchresult_fake [display, gray, linenos]
   "let
   val ctxt0 = @{context}
   val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0
@@ -291,9 +291,9 @@
 
   Often one has the problem that given some terms, create fresh variables
   avoiding any variable occurring in those terms. For this you can use the
-  function @{ML_ind declare_term in Variable} from the structure @{ML_struct Variable}.
+  function @{ML_ind declare_term in Variable} from the structure @{ML_structure Variable}.
 
-  @{ML_response_fake [gray, display]
+  @{ML_matchresult_fake [gray, display]
   "let
   val ctxt1 = Variable.declare_term @{term \"(x, xa)\"} @{context}
   val frees = replicate 2 (\"x\", @{typ nat})
@@ -327,9 +327,9 @@
   All variables are highligted, indicating that they are not
   fixed. However, declaring a term is helpful when parsing terms using
   the function @{ML_ind read_term in Syntax} from the structure
-  @{ML_struct Syntax}. Consider the following code:
+  @{ML_structure Syntax}. Consider the following code:
 
-  @{ML_response_fake [gray, display]
+  @{ML_matchresult_fake [gray, display]
   "let
   val ctxt0 = @{context}
   val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0
@@ -345,7 +345,7 @@
   type the parsed term receives depends upon the last declaration that
   is made, as the next example illustrates.
 
-  @{ML_response_fake [gray, display]
+  @{ML_matchresult_fake [gray, display]
   "let
   val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context}
   val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1
@@ -379,7 +379,7 @@
 
   In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in
   context \<open>ctxt1\<close>.  The function @{ML_ind export_terms in
-  Variable} from the structure @{ML_struct Variable} can be used to transfer
+  Variable} from the structure @{ML_structure Variable} can be used to transfer
   terms between contexts. Transferring means to turn all (free)
   variables that are fixed in one context, but not in the other, into
   schematic variables. In our example, we are transferring the term
@@ -396,11 +396,11 @@
   that the generalisation of fixed variables to schematic variables is
   not trivial if done manually. For illustration purposes we use in the 
   following code the function @{ML_ind make_thm in Skip_Proof} from the 
-  structure @{ML_struct Skip_Proof}. This function will turn an arbitray 
+  structure @{ML_structure Skip_Proof}. This function will turn an arbitray 
   term, in our case @{term "P x y z x y z"}, into a theorem (disregarding 
   whether it is actually provable).
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "let
   val thy = @{theory}
   val ctxt0 = @{context}
@@ -416,9 +416,9 @@
   that exporting from one to another is not just restricted to
   variables, but also works with assumptions. For this we can use the
   function @{ML_ind export in Assumption} from the structure
-  @{ML_struct Assumption}. Consider the following code.
+  @{ML_structure Assumption}. Consider the following code.
 
-  @{ML_response_fake [display, gray, linenos]
+  @{ML_matchresult_fake [display, gray, linenos]
   "let
   val ctxt0 = @{context}
   val ([eq], ctxt1) = Assumption.add_assumes [@{cprop \"x \<equiv> y\"}] ctxt0
@@ -429,11 +429,11 @@
   "x \<equiv> y \<Longrightarrow> y \<equiv> x"}
   
   The function @{ML_ind add_assumes in Assumption} from the structure
-  @{ML_struct Assumption} adds the assumption \mbox{\<open>x \<equiv> y\<close>}
+  @{ML_structure Assumption} adds the assumption \mbox{\<open>x \<equiv> y\<close>}
   to the context \<open>ctxt1\<close> (Line 3). This function expects a list
   of @{ML_type cterm}s and returns them as theorems, together with the
   new context in which they are ``assumed''. In Line 4 we use the
-  function @{ML_ind symmetric in Thm} from the structure @{ML_struct
+  function @{ML_ind symmetric in Thm} from the structure @{ML_structure
   Thm} in order to obtain the symmetric version of the assumed
   meta-equality. Now exporting the theorem \<open>eq'\<close> from \<open>ctxt1\<close> to \<open>ctxt0\<close> means @{term "y \<equiv> x"} will be prefixed with
   the assumed theorem. The boolean flag in @{ML_ind export in
@@ -446,11 +446,11 @@
   Section~\ref{sec:structured}.
 
   The function @{ML_ind export in Proof_Context} from the structure 
-  @{ML_struct Proof_Context} combines both export functions from 
-  @{ML_struct Variable} and @{ML_struct Assumption}. This can be seen
+  @{ML_structure Proof_Context} combines both export functions from 
+  @{ML_structure Variable} and @{ML_structure Assumption}. This can be seen
   in the following example.
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "let
   val ctxt0 = @{context}
   val ((fvs, [eq]), ctxt1) = ctxt0
@@ -589,7 +589,7 @@
   information and qualifiers. Such qualified names can be generated with the
   antiquotation \<open>@{binding \<dots>}\<close>. For example
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
   "@{binding \"name\"}"
   "name"}
 
@@ -634,7 +634,7 @@
   Occasionally you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML_ind  Long_Name.base_name}. For example:
 
-  @{ML_response [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}
+  @{ML_matchresult [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}
 
   \begin{readmore}
   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};




