isabelle-cookbook: comparison ProgTutorial/Essential.thy

equal deleted inserted replaced

-:6103b0eadbf2
+:f7c97e64cc2a
 text \<open>
 In Isabelle, there are certified terms and uncertified terms (respectively types).
 Uncertified terms are often just called terms. One way to construct them is by
 using the antiquotation \mbox{\<open>@{term \<dots>}\<close>}. For example
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "@{term \"(a::nat) + b = c\"}"
 "Const (\"HOL.eq\", _) $
 (Const (\"Groups.plus_class.plus\", _) $ _ $ _) $ _"}
 constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using
 important point of having terms is that you can pattern-match against them;
 this cannot be done with certified terms. As can be seen in Line 5,
 terms use the usual de Bruijn index mechanism for representing bound
 variables.  For example in
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "@{term \"\<lambda>x y. x y\"}"
 "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}
 the indices refer to the number of Abstractions (@{ML Abs}) that we need to
 skip until we hit the @{ML Abs} that binds the corresponding
 term-constructor @{ML $}.
 Be careful if you pretty-print terms. Consider pretty-printing the abstraction
 term shown above:
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "@{term \"\<lambda>x y. x y\"}
 |> pretty_term @{context}
 |> pwriteln"
 "\<lambda>x. x"}
 This is one common source for puzzlement in Isabelle, which has
 tacitly eta-contracted the output. You obtain a similar result
 with beta-redexes
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "let
 val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"}
 val arg1 = @{term \"1::int\"}
 val arg2 = @{term \"2::int\"}
 in
 \ref{sec:printing}), but none for beta-contractions. However you can avoid
 the beta-contractions by switching off abbreviations using the configuration
 value @{ML_ind show_abbrevs in Syntax}. For example
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "let
 val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"}
 val arg1 = @{term \"1::int\"}
 val arg2 = @{term \"2::int\"}
 val ctxt = Config.put show_abbrevs false @{context}
 Isabelle makes a distinction between \emph{free} variables (term-constructor
 @{ML Free} and written on the user level in blue colour) and
 \emph{schematic} variables (term-constructor @{ML Var} and written with a
 leading question mark). Consider the following two examples
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "let
 val v1 = Var ((\"x\", 3), @{typ bool})
 val v2 = Var ((\"x1\", 3), @{typ bool})
 val v3 = Free (\"x\", @{typ bool})
 in
 \end{readmore}
 Constructing terms via antiquotations has the advantage that only typable
 terms can be constructed. For example
-@{ML_response_fake_both [display,gray]
+@{ML_matchresult_fake_both [display,gray]
 "@{term \"x x\"}"
 "Type unification failed: Occurs check!"}
 raises a typing error, while it is perfectly ok to construct the term
 with the raw ML-constructors:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})
 in
 pwriteln (pretty_term @{context} omega)
 end"
 text \<open>
 The antiquotation \<open>@{prop \<dots>}\<close> constructs terms by inserting the
 usually invisible \<open>Trueprop\<close>-coercions whenever necessary.
 Consider for example the pairs
-@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})"
+@{ML_matchresult [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})"
 "(Free (\"P\", _) $ Free (\"x\", _),
 Const (\"HOL.Trueprop\", _) $ (Free (\"P\", _) $ Free (\"x\", _)))"}
 where a coercion is inserted in the second component and
-@{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
+@{ML_matchresult [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
 "(Const (\"Pure.imp\", _) $ _ $ _,
 Const (\"Pure.imp\", _) $ _ $ _)"}
 where it is not (since it is already constructed by a meta-implication).
 The purpose of the \<open>Trueprop\<close>-coercion is to embed formulae of
 is needed whenever a term is constructed that will be proved as a theorem.
 As already seen above, types can be constructed using the antiquotation
 \<open>@{typ _}\<close>. For example:
-@{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
+@{ML_matchresult_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 The corresponding datatype is
 \<close>
 ML_val %grayML\<open>datatype typ =
 like @{typ "int"} or @{typ bool}, are types with an empty list
 of argument types. However, it needs a bit of effort to show an
 example, because Isabelle always pretty prints types (unlike terms).
 Using just the antiquotation \<open>@{typ "bool"}\<close> we only see
-@{ML_response [display, gray]
+@{ML_matchresult [display, gray]
 "@{typ \"bool\"}"
 "bool"}
 which is the pretty printed version of \<open>bool\<close>. However, in PolyML
 (version \<open>\<ge>\<close>5.3) it is easy to install your own pretty printer. With the
 function below we mimic the behaviour of the usual pretty printer for
 ML \<open>@{typ "bool"}\<close>
 text \<open>
 Now the type bool is printed out in full detail.
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "@{typ \"bool\"}"
 "Type (\"HOL.bool\", [])"}
 When printing out a list-type
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "@{typ \"'a list\"}"
 "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"}
 we can see the full name of the type is actually \<open>List.list\<close>, indicating
 that it is defined in the theory \<open>List\<close>. However, one has to be
 careful with names of types, because even if
 \<open>fun\<close> is defined in the theory \<open>HOL\<close>, it is
 still represented by its simple name.
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "@{typ \"bool \<Rightarrow> nat\"}"
 "Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"}
 We can restore the usual behaviour of Isabelle's pretty printer
 with the code
 text \<open>
 After that the types for booleans, lists and so on are printed out again
 the standard Isabelle way.
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "@{typ \"bool\"};
 @{typ \"'a list\"}"
 "\"bool\"
 \"'a List.list\""}
 text \<open>
 To see this, apply \<open>@{term S}\<close> and \<open>@{term T}\<close>
 to both functions. With @{ML make_imp} you obtain the intended term involving
 the given arguments
-@{ML_response [display,gray] "make_imp @{term S} @{term T}"
+@{ML_matchresult [display,gray] "make_imp @{term S} @{term T}"
 "Const _ $
 Abs (\"x\", Type (\"Nat.nat\",[]),
 Const _ $ (Free (\"S\",_) $ _) $ (Free (\"T\",_) $ _))"}
 whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"}
 and \<open>Q\<close> from the antiquotation.
-@{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}"
+@{ML_matchresult [display,gray] "make_wrong_imp @{term S} @{term T}"
 "Const _ $
 Abs (\"x\", _,
 Const _ $ (Const _ $ (Free (\"P\",_) $ _)) $
 (Const _ $ (Free (\"Q\",_) $ _)))"}
 constructing terms. One is the function @{ML_ind list_comb in Term}, which
 takes as argument a term and a list of terms, and produces as output the
 term list applied to the term. For example
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val trm = @{term \"P::bool \<Rightarrow> bool \<Rightarrow> bool\"}
 val args = [@{term \"True\"}, @{term \"False\"}]
 in
 list_comb (trm, args)
 $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
 Another handy function is @{ML_ind lambda in Term}, which abstracts a variable
 in a term. For example
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val x_nat = @{term \"x::nat\"}
 val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
 in
 lambda x_nat trm
 variable and for printing purposes also its name.  Note that because of the
 typing annotation on \<open>P\<close>, the variable \<open>x\<close> in \<open>P x\<close>
 is of the same type as the abstracted variable. If it is of different type,
 as in
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val x_int = @{term \"x::int\"}
 val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
 in
 lambda x_int trm
 There is also the function @{ML_ind subst_free in Term} with which terms can be
 replaced by other terms. For example below, we will replace in @{term
 "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by
 @{term y}, and @{term x} by @{term True}.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val sub1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
 val sub2 = (@{term \"x::nat\"}, @{term \"True\"})
 val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
 in
 "Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}
 As can be seen, @{ML subst_free} does not take typability into account.
 However it takes alpha-equivalence into account:
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "let
 val sub = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})
 val trm = @{term \"(\<lambda>x::nat. x)\"}
 in
 subst_free [sub] trm
 text \<open>
 The function returns a pair consisting of the stripped off variables and
 the body of the universal quantification. For example
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
 "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
 Const (\"op =\", _) $ Bound 1 $ Bound 0)"}
 Note that we produced in the body two dangling de Bruijn indices.
 text \<open>
 As said above, after calling @{ML strip_alls}, you obtain a term with loose
 bound variables. With the function @{ML subst_bounds}, you can replace these
 loose @{ML_ind Bound in Term}s with the stripped off variables.
-@{ML_response_fake [display, gray, linenos]
+@{ML_matchresult_fake [display, gray, linenos]
 "let
 val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
 in
 subst_bounds (rev vrs, trm)
 |> pretty_term @{context}
 name is by no means unique. If clashes need to be avoided, then we should
 use the function @{ML_ind dest_abs in Term}, which returns the body where
 the loose de Bruijn index is replaced by a unique free variable. For example
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val body = Bound 0 $ Free (\"x\", @{typ nat})
 in
 Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body)
 end"
 Sometimes it is necessary to manipulate de Bruijn indices in terms directly.
 There are many functions to do this. We describe only two. The first,
 @{ML_ind incr_boundvars in Term}, increases by an integer the indices
 of the loose bound variables in a term. In the code below
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "@{term \"\<forall>x y z u. z = u\"}
 |> strip_alls
 ||> incr_boundvars 2
 |> build_alls
 |> pretty_term @{context}
 between the first two quantified variables.
 The second function, @{ML_ind loose_bvar1 in Text}, tests whether a term
 contains a loose bound of a certain index. For example
-@{ML_response_fake [gray,display]
+@{ML_matchresult_fake [gray,display]
 "let
 val body = snd (strip_alls @{term \"\<forall>x y. x = (y::bool)\"})
 in
 [loose_bvar1 (body, 0),
 loose_bvar1 (body, 1),
 loose_bvar1 (body, 2)]
 end"
 "[true, true, false]"}
 There are also many convenient functions that construct specific HOL-terms
-in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in
+in the structure @{ML_structure HOLogic}. For example @{ML_ind mk_eq in
 HOLogic} constructs an equality out of two terms.  The types needed in this
 equality are calculated from the type of the arguments. For example
-@{ML_response_fake [gray,display]
+@{ML_matchresult_fake [gray,display]
 "let
 val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
 in
 eq |> pretty_term @{context}
 |> pwriteln
 | is_all _ = false\<close>
 text \<open>
 will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}:
-@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
+@{ML_matchresult [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
 The problem is that the \<open>@term\<close>-antiquotation in the pattern
 fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for
 an arbitrary, but fixed type @{typ "'a"}. A properly working alternative
 for this function is
 | is_all _ = false\<close>
 text \<open>
 because now
-@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
+@{ML_matchresult [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
 matches correctly (the first wildcard in the pattern matches any type and the
 second any term).
 However there is still a problem: consider the similar function that
 | is_nil _ = false\<close>
 text \<open>
 Unfortunately, also this function does \emph{not} work as expected, since
-@{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
+@{ML_matchresult [display,gray] "is_nil @{term \"Nil\"}" "false"}
 The problem is that on the ML-level the name of a constant is more
 subtle than you might expect. The function @{ML is_all} worked correctly,
 because @{term "All"} is such a fundamental constant, which can be referenced
 by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
-@{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", _)"}
+@{ML_matchresult [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", _)"}
 the name of the constant \<open>Nil\<close> depends on the theory in which the
 term constructor is defined (\<open>List\<close>) and also in which datatype
 (\<open>list\<close>). Even worse, some constants have a name involving
 type-classes. Consider for example the constants for @{term "zero"} and
 \mbox{@{term "times"}}:
-@{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})"
+@{ML_matchresult [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})"
 "(Const (\"Groups.zero_class.zero\", _),
 Const (\"Groups.times_class.times\", _))"}
 While you could use the complete name, for example
 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
 text \<open>
 The antiquotation for properly referencing type constants is \<open>@{type_name \<dots>}\<close>.
 For example
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "@{type_name \"list\"}" "\"List.list\""}
 Although types of terms can often be inferred, there are many
 situations where you need to construct types manually, especially
 when defining constants. For example the function returning a function
 | _ => ty)\<close>
 text \<open>
 Here is an example:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "map_types nat_to_int @{term \"a = (1::nat)\"}"
 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
 If you want to obtain the list of free type-variables of a term, you
 that is they take, besides a term, also a list of type-variables as input.
 So in order to obtain the list of type-variables of a term you have to
 call them as follows
-@{ML_response [gray,display]
+@{ML_matchresult [gray,display]
 "Term.add_tfrees @{term \"(a, b)\"} []"
 "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
 The reason for this definition is that @{ML add_tfrees in Term} can
 be easily folded over a list of terms. Similarly for all functions
 schematic variables.
 Let us begin with describing the unification and matching functions for
 types.  Both return type environments (ML-type @{ML_type "Type.tyenv"})
 which map schematic type variables to types and sorts. Below we use the
-function @{ML_ind typ_unify in Sign} from the structure @{ML_struct Sign}
+function @{ML_ind typ_unify in Sign} from the structure @{ML_structure Sign}
 for unifying the types \<open>?'a * ?'b\<close> and \<open>?'b list *
 nat\<close>. This will produce the mapping, or type environment, \<open>[?'a :=
 ?'b list, ?'b := nat]\<close>.
 \<close>
 environment, which is needed for starting the unification without any
 (pre)instantiations. The \<open>0\<close> is an integer index that will be explained
 below. In case of failure, @{ML typ_unify in Sign} will raise the exception
 \<open>TUNIFY\<close>.  We can print out the resulting type environment bound to
 @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
-structure @{ML_struct Vartab}.
+structure @{ML_structure Vartab}.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "Vartab.dest tyenv_unif"
 "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")),
 ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"}
 \<close>
 use in what follows our own pretty-printing function from
 Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type
 environment in the example this function prints out the more legible:
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "pretty_tyenv @{context} tyenv_unif"
 "[?'a := ?'b list, ?'b := nat]"}
 The way the unification function @{ML typ_unify in Sign} is implemented
 using an initial type environment and initial index makes it easy to
 text \<open>
 To print out the result type environment we switch on the printing
 of sort information by setting @{ML_ind show_sorts in Syntax} to
 true. This allows us to inspect the typing environment.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "pretty_tyenv @{context} tyenv"
 "[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]"}
 As can be seen, the type variables \<open>?'a\<close> and \<open>?'b\<close> are instantiated
 with a new type variable \<open>?'a1\<close> with sort \<open>{s1, s2}\<close>. Since a new
 type variable has been introduced the @{ML index}, originally being \<open>0\<close>,
 has been increased to \<open>1\<close>.
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "index"
 "1"}
 Let us now return to the unification problem \<open>?'a * ?'b\<close> and
 \<open>?'b list * nat\<close> from the beginning of this section, and the
 calculated type environment @{ML tyenv_unif}:
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "pretty_tyenv @{context} tyenv_unif"
 "[?'a := ?'b list, ?'b := nat]"}
 Observe that the type environment which the function @{ML typ_unify in
 Sign} returns is \emph{not} an instantiation in fully solved form: while \<open>?'b\<close> is instantiated to @{typ nat}, this is not propagated to the
 called an instantiation in \emph{triangular form}. These triangular
 instantiations, or triangular type environments, are used because of
 performance reasons. To apply such a type environment to a type, say \<open>?'a *
 ?'b\<close>, you should use the function @{ML_ind norm_type in Envir}:
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
 "nat list * nat"}
 Matching of types can be done with the function @{ML_ind typ_match in Sign}
-also from the structure @{ML_struct Sign}. This function returns a @{ML_type
+also from the structure @{ML_structure Sign}. This function returns a @{ML_type
 Type.tyenv} as well, but might raise the exception \<open>TYPE_MATCH\<close> in case
 of failure. For example
 \<close>
 ML %grayML\<open>val tyenv_match = let
 end\<close>
 text \<open>
 Printing out the calculated matcher gives
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "pretty_tyenv @{context} tyenv_match"
 "[?'a := bool list, ?'b := nat]"}
 Unlike unification, which uses the function @{ML norm_type in Envir},
 applying the matcher to a type needs to be done with the function
 @{ML_ind subst_type in Envir}. For example
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
 "bool list * nat"}
 Be careful to observe the difference: always use
 @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir}
 text \<open>
 Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. If we apply
 @{ML norm_type in Envir} to the type \<open>?'a * ?'b\<close> we obtain
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"
 "nat list * nat"}
 which does not solve the matching problem, and if
 we apply @{ML subst_type in Envir} to the same type we obtain
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
 "?'b list * nat"}
 which does not solve the unification problem.
 text \<open>
 In this example we annotated types explicitly because then
 the type environment is empty and can be ignored. The
 resulting term environment is
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "pretty_env @{context} fo_env"
 "[?X := P, ?Y := \<lambda>a b. Q b a]"}
 The matcher can be applied to a term using the function @{ML_ind subst_term
 in Envir} (remember the same convention for types applies to terms: @{ML
 subst_term in Envir} is for matchers and @{ML norm_term in Envir} for
 unifiers). The function @{ML subst_term in Envir} expects a type environment,
 which is set to empty in the example below, and a term environment.
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "let
 val trm = @{term_pat \"(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y\"}
 in
 Envir.subst_term (Vartab.empty, fo_env) trm
 |> pretty_term @{context}
 alpha-equivalence, but this kind of matching should be used with care, since
 it is not clear whether the result is meaningful. A meaningful example is
 matching \<open>\<lambda>x. P x\<close> against the pattern \<open>\<lambda>y. ?X y\<close>. In this
 case, first-order matching produces \<open>[?X := P]\<close>.
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "let
 val fo_pat = @{term_pat \"\<lambda>y. (?X::nat\<Rightarrow>bool) y\"}
 val trm = @{term \"\<lambda>x. (P::nat\<Rightarrow>bool) x\"}
 val init = (Vartab.empty, Vartab.empty)
 in
 \emph{\index*{pattern}} is a well-formed term in which the arguments to
 every schematic variable are distinct bounds.
 In particular this excludes terms where a
 schematic variable is an argument of another one and where a schematic
 variable is applied twice with the same bound variable. The function
-@{ML_ind pattern in Pattern} in the structure @{ML_struct Pattern} tests
+@{ML_ind pattern in Pattern} in the structure @{ML_structure Pattern} tests
 whether a term satisfies these restrictions under the assumptions
 that it is beta-normal, well-typed and has no loose bound variables.
-@{ML_response [display, gray]
+@{ML_matchresult [display, gray]
 "let
 val trm_list =
 [@{term_pat \"?X\"}, @{term_pat \"a\"},
 @{term_pat \"f (\<lambda>a b. ?X a b) c\"},
 @{term_pat \"\<lambda>a b. (+) a b\"},
 In this way, matching and unification can be implemented as functions that
 produce a type and term environment (unification actually returns a
 record of type @{ML_type Envir.env} containing a max-index, a type environment
 and a term environment). The corresponding functions are @{ML_ind match in Pattern}
 and @{ML_ind unify in Pattern}, both implemented in the structure
-@{ML_struct Pattern}. An example for higher-order pattern unification is
+@{ML_structure Pattern}. An example for higher-order pattern unification is
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "let
 val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}
 val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}
 val init = Envir.empty 0
 val env = Pattern.unify (Context.Proof @{context}) (trm1, trm2) init (* FIXME: Reference to generic context *)
 text \<open>
 \footnote{\bf FIXME: what is the list of term pairs in the unifier: flex-flex pairs?}
 We can print them out as follows.
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "pretty_env @{context} (Envir.term_env un1);
 pretty_env @{context} (Envir.term_env un2);
 pretty_env @{context} (Envir.term_env un3)"
 "[?X := \<lambda>a. a, ?Y := f a]
 [?X := f, ?Y := a]
 In case of failure the function @{ML_ind unifiers in Unify} does not raise
 an exception, rather returns the empty sequence. For example
-@{ML_response [display, gray]
+@{ML_matchresult [display, gray]
 "let
 val trm1 = @{term \"a\"}
 val trm2 = @{term \"b\"}
 val init = Envir.empty 0
 in
 also tries first to solve the problem by higher-order pattern
 unification. Only in case of failure full higher-order unification is
 called. This function has a built-in bound, which can be accessed and
 manipulated as a configuration value. For example
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "Config.get_global @{theory} (Unify.search_bound)"
 "Int 60"}
 If this bound is reached during unification, Isabelle prints out the
 warning message @{text [quotes] "Unification bound exceeded"} and
 plenty of diagnostic information (sometimes annoyingly plenty of
 information).
 For higher-order matching the function is called @{ML_ind matchers in Unify}
-implemented in the structure @{ML_struct Unify}. Also this function returns
+implemented in the structure @{ML_structure Unify}. Also this function returns
 sequences with possibly more than one matcher.  Like @{ML unifiers in
 Unify}, this function does not raise an exception in case of failure, but
 returns an empty sequence. It also first tries out whether the matching
 problem can be solved by first-order matching.
 as an introduction rule. Applying it directly can lead to unexpected
 behaviour since the unification has more than one solution. One way round
 this problem is to instantiate the schematic variables \<open>?P\<close> and
 \<open>?x\<close>.  Instantiation function for theorems is
 @{ML_ind instantiate_normalize in Drule} from the structure
-@{ML_struct Drule}. One problem, however, is
+@{ML_structure Drule}. One problem, however, is
 that this function expects the instantiations as lists of @{ML_type "((indexname * sort) * ctyp)"}
 respective @{ML_type "(indexname * typ) * cterm"}:
 \begin{isabelle}
 @{ML instantiate_normalize in Drule}\<open>:\<close>
 environments (Line 8). As a simple example we instantiate the
 @{thm [source] spec} rule so that its conclusion is of the form
 @{term "Q True"}.
-@{ML_response_fake [gray,display,linenos]
+@{ML_matchresult_fake [gray,display,linenos]
 "let
 val pat = Logic.strip_imp_concl (Thm.prop_of @{thm spec})
 val trm = @{term \"Trueprop (Q True)\"}
 val inst = matcher_inst @{context} pat trm 1
 in
 enough typing information (constants, free variables and abstractions all have typing
 information) so that it is always clear what the type of a term is.
 Given a well-typed term, the function @{ML_ind type_of in Term} returns the
 type of a term. Consider for example:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 To calculate the type, this function traverses the whole term and will
 detect any typing inconsistency. For example changing the type of the variable
 @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})"
 "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
 Since the complete traversal might sometimes be too costly and
 not necessary, there is the function @{ML_ind fastype_of in Term}, which
 also returns the type of a term.
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 However, efficiency is gained on the expense of skipping some tests. You
 can see this in the following example
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
 where no error is detected.
 Sometimes it is a bit inconvenient to construct a term with
 information is redundant. A short-cut is to use the ``place-holder''
 type @{ML_ind dummyT in Term} and then let type-inference figure out the
 complete type. The type inference can be invoked with the function
 @{ML_ind check_term in Syntax}. An example is as follows:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val c = Const (@{const_name \"plus\"}, dummyT)
 val o = @{term \"1::nat\"}
 val v = Free (\"x\", dummyT)
 in
 be constructed via ``official interfaces''.
 Certification is always relative to a context. For example you can
 write:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "Thm.cterm_of @{context} @{term \"(a::nat) + b = c\"}"
 "a + b = c"}
 This can also be written with an antiquotation:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "@{cterm \"(a::nat) + b = c\"}"
 "a + b = c"}
 Attempting to obtain the certified term for
-@{ML_response_fake_both [display,gray]
+@{ML_matchresult_fake_both [display,gray]
 "@{cterm \"1 + True\"}"
 "Type unification failed \<dots>"}
 yields an error (since the term is not typable). A slightly more elaborate
 example that type-checks is:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val natT = @{typ \"nat\"}
 val zero = @{term \"0::nat\"}
 val plus = Const (@{const_name plus}, [natT, natT] ---> natT)
 in
 In Isabelle not just terms need to be certified, but also types. For example,
 you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on
 the ML-level as follows:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})"
 "nat \<Rightarrow> bool"}
 or with the antiquotation:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "@{ctyp \"nat \<Rightarrow> bool\"}"
 "nat \<Rightarrow> bool"}
 Since certified terms are, unlike terms, abstract objects, we cannot
 pattern-match against them. However, we can construct them. For example
 the function @{ML_ind apply in Thm} produces a certified application.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "Thm.apply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
 "P 3"}
-Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_struct Drule}
+Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_structure Drule}
 applies a list of @{ML_type cterm}s.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val chead = @{cterm \"P::unit \<Rightarrow> nat \<Rightarrow> bool\"}
 val cargs = [@{cterm \"()\"}, @{cterm \"3::nat\"}]
 in
 Drule.list_comb (chead, cargs)
 inserts necessary \<open>Trueprop\<close>s.
 If we print out the value of @{ML my_thm} then we see only the
 final statement of the theorem.
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "pwriteln (pretty_thm @{context} my_thm)"
 "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 However, internally the code-snippet constructs the following
 proof.
 While we obtained a theorem as result, this theorem is not
 yet stored in Isabelle's theorem database. Consequently, it cannot be
 referenced on the user level. One way to store it in the theorem database is
 by using the function @{ML_ind note in Local_Theory} from the structure
-@{ML_struct Local_Theory} (the Isabelle command
+@{ML_structure Local_Theory} (the Isabelle command
 \isacommand{local\_setup} will be explained in more detail in
 Section~\ref{sec:local}).
 \<close>
 (*FIXME: add forward reference to Proof_Context.export *)
 text \<open>
 Note that we have to use another name under which the theorem is stored,
 since Isabelle does not allow us to call  @{ML_ind note in Local_Theory} twice
 with the same name. The attribute needs to be wrapped inside the function @{ML_ind
-internal in Attrib} from the structure @{ML_struct Attrib}. If we use the function
+internal in Attrib} from the structure @{ML_structure Attrib}. If we use the function
 @{ML get_thm_names_from_ss} from
 the previous chapter, we can check whether the theorem has actually been
 added.
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "let
 fun pred s = match_string \"my_thm_simp\" s
 in
 exists pred (get_thm_names_from_ss @{context})
 end"
 and   thm3: "\<forall>y. Q y" sorry
 text \<open>
 Testing them for alpha equality produces:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),
 Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))"
 "(true, false)"}
 Many functions destruct theorems into @{ML_type cterm}s. For example
 the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return
 the left and right-hand side, respectively, of a meta-equality.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val eq = @{thm True_def}
 in
 (Thm.lhs_of eq, Thm.rhs_of eq)
 |> apply2 (Pretty.string_of o (pretty_cterm @{context}))
 and   foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry
 text \<open>
 We can destruct them into premises and conclusions as follows.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val ctxt = @{context}
 fun prems_and_concl thm =
 [[Pretty.str \"Premises:\", pretty_terms ctxt (Thm.prems_of thm)],
 [Pretty.str \"Conclusion:\", pretty_term ctxt (Thm.concl_of thm)]]
 Section~\ref{sec:simplifier}, the simplifier
 can be used to work directly over theorems, for example to unfold definitions. To show
 this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then
 unfold the constant @{term "True"} according to its definition (Line 2).
-@{ML_response_fake [display,gray,linenos]
+@{ML_matchresult_fake [display,gray,linenos]
 "Thm.reflexive @{cterm \"True\"}
 |> Simplifier.rewrite_rule @{context} [@{thm True_def}]
 |> pretty_thm @{context}
 |> pwriteln"
 "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
 from the meta logic are more convenient for reasoning. Therefore there are
 some build in functions which help with these transformations. The function
 @{ML_ind rulify in Object_Logic}
 replaces all object connectives by equivalents in the meta logic. For example
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "Object_Logic.rulify @{context} @{thm foo_test2}"
 "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"}
 The transformation in the other direction can be achieved with function
 @{ML_ind atomize in Object_Logic} and the following code.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val thm = @{thm foo_test1}
 val meta_eq = Object_Logic.atomize @{context} (Thm.cprop_of thm)
 in
 Raw_Simplifier.rewrite_rule @{context} [meta_eq] thm
 end\<close>
 text \<open>
 This function produces for the theorem @{thm [source] list.induct}
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "atomize_thm @{context} @{thm list.induct}"
 "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
 Theorems can also be produced from terms by giving an explicit proof.
 One way to achieve this is by using the function @{ML_ind prove in Goal}
-in the structure @{ML_struct Goal}. For example below we use this function
+in the structure @{ML_structure Goal}. For example below we use this function
 to prove the term @{term "P \<Longrightarrow> P"}.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val trm = @{term \"P \<Longrightarrow> P::bool\"}
 val tac = K (assume_tac @{context} 1)
 in
 Goal.prove @{context} [\"P\"] [] trm tac
 text \<open>
 With them we can now produce three theorem instances of the
 proposition.
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "multi_test @{context} 3"
 "[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"}
 However you should be careful with @{ML prove_common in Goal} and very
 large goals. If you increase the counter in the code above to \<open>3000\<close>,
 end\<close>
 text \<open>
 While the LCF-approach of going through interfaces ensures soundness in Isabelle, there
 is the function @{ML_ind make_thm in Skip_Proof} in the structure
-@{ML_struct Skip_Proof} that allows us to turn any proposition into a theorem.
+@{ML_structure Skip_Proof} that allows us to turn any proposition into a theorem.
 Potentially making the system unsound.  This is sometimes useful for developing
 purposes, or when explicit proof construction should be omitted due to performace
 reasons. An example of this function is as follows:
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"
 "True = False"}
 \begin{readmore}
 Functions that setup goal states and prove theorems are implemented in
 text \<open>
 The auxiliary data of this lemma can be retrieved using the function
 @{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "Thm.get_tags @{thm foo_data}"
 "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}
 consisting of a name and a kind.  When we store lemmas in the theorem database,
 we might want to explicitly extend this data by attaching case names to the
 two premises of the lemma.  This can be done with the function @{ML_ind name in Rule_Cases}
-from the structure @{ML_struct Rule_Cases}.
+from the structure @{ML_structure Rule_Cases}.
 \<close>
 local_setup %gray \<open>
 Local_Theory.note ((@{binding "foo_data'"}, []),
 [(Rule_Cases.name ["foo_case_one", "foo_case_two"]
 @{thm foo_data})]) #> snd\<close>
 text \<open>
 The data of the theorem @{thm [source] foo_data'} is then as follows:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "Thm.get_tags @{thm foo_data'}"
 "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"),
 (\"case_names\", \"foo_case_one;foo_case_two\")]"}
 You can observe the case names of this lemma on the user level when using
 text \<open>
 Sometimes one wants to know the theorems that are involved in
 proving a theorem, especially when the proof is by \<open>auto\<close>. These theorems can be obtained by introspecting the proved theorem.
 To introspect a theorem, let us define the following three functions
 that analyse the @{ML_type_ind proof_body} data-structure from the
-structure @{ML_struct Proofterm}.
+structure @{ML_structure Proofterm}.
 \<close>
 ML %grayML\<open>fun pthms_of (PBody {thms, ...}) = map #2 thms
 val get_names = (map Proofterm.thm_node_name) o pthms_of
 val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of\<close>
 a proof-tree that records all theorems that are employed for
 establishing this theorem.  We can traverse this proof-tree
 extracting this information.  Let us first extract the name of the
 established theorem. This can be done with
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "@{thm my_conjIa}
 |> Thm.proof_body_of
 |> get_names"
 "[\"Essential.my_conjIa\"]"}
 theorem.  Notice that the first proof above references
 three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1}
 and @{thm [source] conjunct2}. We can obtain them by descending into the
 first level of the proof-tree, as follows.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "@{thm my_conjIa}
 |> Thm.proof_body_of
 |> get_pbodies
 |> map get_names
 |> List.concat"
 The theorems @{thm [source] Pure.protectD} and @{thm [source]
 Pure.protectI} that are internal theorems are always part of a
 proof in Isabelle. Note also that applications of \<open>assumption\<close> do not
 count as a separate theorem, as you can see in the following code.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "@{thm my_conjIb}
 |> Thm.proof_body_of
 |> get_pbodies
 |> map get_names
 |> List.concat"
 Interestingly, but not surprisingly, the proof of @{thm [source]
 my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
 and @{thm [source] my_conjIb}, as can be seen by the theorems that
 are returned for @{thm [source] my_conjIc}.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "@{thm my_conjIc}
 |> Thm.proof_body_of
 |> get_pbodies
 |> map get_names
 |> List.concat"
 Of course we can also descend into the second level of the tree
 ``behind'' @{thm [source] my_conjIa} say, which
 means we obtain the theorems that are used in order to prove
 @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
-@{ML_response_fake [display, gray]
+@{ML_matchresult_fake [display, gray]
 "@{thm my_conjIa}
 |> Thm.proof_body_of
 |> get_pbodies
 |> map get_pbodies
 |> (map o map) get_names
 lemma trueI_2[my_thms]: "True" by simp
 text \<open>
 then you can see it is added to the initially empty list.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "MyThms.get @{context}"
 "[\"True\"]"}
 You can also add theorems using the command \isacommand{declare}.
 \<close>
 text \<open>
 With this attribute, the \<open>add\<close> operation is the default and does
 not need to be explicitly given. These three declarations will cause the
 theorem list to be updated as:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "MyThms.get @{context}"
 "[\"True\", \"Suc (Suc 0) = 2\"]"}
 The theorem @{thm [source] trueI_2} only appears once, since the
 function @{ML_ind  add_thm in Thm} tests for duplicates, before extending
 declare test[my_thms del]
 text \<open>After this, the theorem list is again:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "MyThms.get @{context}"
 "[\"True\"]"}
 We used in this example two functions declared as @{ML_ind
 declaration_attribute in Thm}, but there can be any number of them. We just
 @{ML_type_ind [display, gray] "Pretty.T"}
 The function @{ML str in Pretty} transforms a (plain) string into such a pretty
 type. For example
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "Pretty.str \"test\"" "String (\"test\", 4)"}
 where the result indicates that we transformed a string with length 4. Once
 you have a pretty type, you can, for example, control where linebreaks may
 occur in case the text wraps over a line, or with how much indentation a
 text \<open>
 We deliberately chose a large string so that it spans over more than one line.
 If we print out the string using the usual ``quick-and-dirty'' method, then
 we obtain the ugly output:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "tracing test_str"
 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
 oooooooooooooobaaaaaaaaaaaar"}
 We obtain the same if we just use the function @{ML pprint}.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "pprint (Pretty.str test_str)"
 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
 oooooooooooooobaaaaaaaaaaaar"}
 function @{ML_ind breaks in Pretty}, which expects a list of pretty types
 and inserts a possible line break in between every two elements in this
 list. To print this list of pretty types as a single string, we concatenate
 them with the function @{ML_ind blk in Pretty} as follows:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val ptrs = map Pretty.str (space_explode \" \" test_str)
 in
 pprint (Pretty.blk (0, Pretty.breaks ptrs))
 end"
 Here the layout of @{ML test_str} is much more pleasing to the
 eye. The @{ML "0"} in @{ML_ind  blk in Pretty} stands for no hanging
 indentation of the printed string. You can increase the indentation
 and obtain
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val ptrs = map Pretty.str (space_explode \" \" test_str)
 in
 pprint (Pretty.blk (3, Pretty.breaks ptrs))
 end"
 where starting from the second line the indent is 3. If you want
 that every line starts with the same indent, you can use the
 function @{ML_ind  indent in Pretty} as follows:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val ptrs = map Pretty.str (space_explode \" \" test_str)
 in
 pprint (Pretty.indent 10 (Pretty.blk (0, Pretty.breaks ptrs)))
 end"
 If you want to print out a list of items separated by commas and
 have the linebreaks handled properly, you can use the function
 @{ML_ind  commas in Pretty}. For example
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
 in
 pprint (Pretty.blk (0, Pretty.commas ptrs))
 end"
 @{ML_ind  enum in Pretty}. For example
 \<close>
 text \<open>
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
 in
 pprint (Pretty.enum \",\" \"{\" \"}\" ptrs)
 end"
 to insert a space (of length 1) before the
 @{text [quotes] "and"}. This space is also a place where a line break
 can occur. We do the same after the @{text [quotes] "and"}. This gives you
 for example
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22)
 val ptrs2 = map (Pretty.str o string_of_int) (10 upto 28)
 in
 pprint (Pretty.blk (0, and_list ptrs1));
 Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out
 a list of items, but automatically inserts forced breaks between each item.
 Compare
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
 in
 pprint (Pretty.blk (0, a_and_b));
 pprint (Pretty.chunks a_and_b)
 The function @{ML_ind big_list in Pretty} helps with printing long lists.
 It is used for example in the command \isacommand{print\_theorems}. An
 example is as follows.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
 val pstrs = map (Pretty.str o string_of_int) (4 upto 10)
 in
 pprint (Pretty.big_list \"header\" pstrs)
 end"
 The point of the pretty-printing functions is to conveninetly obtain
 a lay-out of terms and types that is pleasing to the eye. If we print
 out the the terms produced by the the function @{ML de_bruijn} from
 exercise~\ref{ex:debruijn} we obtain the following:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "pprint (Syntax.pretty_term  @{context} (de_bruijn 4))"
 "(P 3 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
 (P 2 = P 3 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
 (P 1 = P 2 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
 (P 1 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<longrightarrow>
 Pretty} in order to enclose the term and type inside quotation marks. In
 Line 9 we add a period right after the type without the possibility of a
 line break, because we do not want that a line break occurs there.
 Now you can write
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "tell_type @{context} @{term \"min (Suc 0)\"}"
 "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
 To see the proper line breaking, you can try out the function on a bigger term
 and type. For example:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "tell_type @{context} @{term \"(=) ((=) ((=) ((=) ((=) (=)))))\"}"
 "The term \"(=) ((=) ((=) ((=) ((=) (=)))))\" has type
 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
 \begin{readmore}

changeset 567	f7c97e64cc2a
parent 566	6103b0eadbf2
child 569	f875a25aa72d