# HG changeset patch
# User wenzelm
# Date 1393244210 -3600
# Node ID bc04f1ab3c3a54c7ea4f50aae06aef6bdf597bd4
# Parent  ed1b789d0b213668571a8f816c80027727980490
tuned messages -- prefer quote before Position.here, which might be just \<here>;

diff -r ed1b789d0b21 -r bc04f1ab3c3a src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Mon Feb 24 13:10:33 2014 +0100
+++ b/src/Tools/induct_tacs.ML	Mon Feb 24 13:16:50 2014 +0100
@@ -23,7 +23,8 @@
     val u = singleton (Variable.polymorphic ctxt) t;
     val U = Term.fastype_of u;
     val _ = Term.is_TVar U andalso
-      error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u ^ Position.here pos);
+      error ("Cannot determine type of " ^
+        quote (Syntax.string_of_term ctxt u) ^ Position.here pos);
   in (u, U) end;
 
 fun gen_case_tac ctxt0 s opt_rule i st =
@@ -75,17 +76,17 @@
         val pos = Syntax.read_token_pos name;
         val (x, _) = Term.dest_Free t handle TERM _ =>
           error ("Induction argument not a variable: " ^
-            Syntax.string_of_term ctxt t ^ Position.here pos);
+            quote (Syntax.string_of_term ctxt t) ^ Position.here pos);
         val eq_x = fn Free (y, _) => x = y | _ => false;
         val _ =
           if Term.exists_subterm eq_x concl then ()
           else
             error ("No such variable in subgoal: " ^
-              Syntax.string_of_term ctxt t ^ Position.here pos);
+              quote (Syntax.string_of_term ctxt t) ^ Position.here pos);
         val _ =
           if (exists o Term.exists_subterm) eq_x prems then
             warning ("Induction variable occurs also among premises: " ^
-              Syntax.string_of_term ctxt t ^ Position.here pos)
+              quote (Syntax.string_of_term ctxt t) ^ Position.here pos)
           else ();
       in #1 (check_type ctxt (t, pos)) end;