--- a/src/Doc/Isar_Ref/Generic.thy Mon Oct 12 20:25:08 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Mon Oct 12 20:25:50 2015 +0200
@@ -1574,8 +1574,8 @@
\item Function variables may only be applied to parameters of the
subgoal. (This restriction arises because the prover does not use
higher-order unification.) If other function variables are present
- then the prover will fail with the message \texttt{Function Var's
- argument not a bound variable}.
+ then the prover will fail with the message
+ @{verbatim [display] \<open>Function unknown's argument not a bound variable\<close>}
\item Its proof strategy is more general than @{method fast} but can
be slower. If @{method blast} fails or seems to be running forever,
--- a/src/Provers/blast.ML Mon Oct 12 20:25:08 2015 +0200
+++ b/src/Provers/blast.ML Mon Oct 12 20:25:50 2015 +0200
@@ -18,7 +18,7 @@
* ignores elimination rules that don't have the correct format
(conclusion must be a formula variable)
* rules must not require higher-order unification, e.g. apply_type in ZF
- + message "Function Var's argument not a bound variable" relates to this
+ + message "Function unknown's argument not a bound variable" relates to this
* its proof strategy is more general but can actually be slower
Known problems: