src/Tools/induct_tacs.ML

 fun check_type ctxt (t, pos) =
   let
     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 =
   let
     val (_, ctxt) = Variable.focus_subgoal i st ctxt0;

       let
         val t = Syntax.read_term ctxt name;
         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;
 
     val argss = map (map (Option.map induct_var)) varss;
     val rule =