# HG changeset patch
# User wenzelm
# Date 1444674350 -7200
# Node ID 6d892287d0e90ffcb881d9d4c6d64abf11c61884
# Parent  bbe9ae2c9289c77185903a5a276d8562548cf3db
proper message;

diff -r bbe9ae2c9289 -r 6d892287d0e9 src/Doc/Isar_Ref/Generic.thy
--- 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,
diff -r bbe9ae2c9289 -r 6d892287d0e9 src/Provers/blast.ML
--- 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: