# HG changeset patch
# User blanchet
# Date 1392582808 -3600
# Node ID 9429e7b5b8273d4d491ab93da5154e0a8e724177
# Parent  23d2cbac6dce59c57562dcb8c4d03d424fe47206
removed final periods in messages for proof methods

diff -r 23d2cbac6dce -r 9429e7b5b827 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Sun Feb 16 21:09:47 2014 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sun Feb 16 21:33:28 2014 +0100
@@ -172,9 +172,8 @@
       val eqth = introduce_combinators_in_cterm (cprop_of th)
     in Thm.equal_elim eqth th end
     handle THM (msg, _, _) =>
-           (warning ("Error in the combinator translation of " ^
-                     Display.string_of_thm ctxt th ^
-                     "\nException message: " ^ msg ^ ".");
+           (warning ("Error in the combinator translation of " ^ Display.string_of_thm ctxt th ^
+              "\nException message: " ^ msg);
             (* A type variable of sort "{}" will make "abstraction" fail. *)
             TrueI)
 
diff -r 23d2cbac6dce -r 9429e7b5b827 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Feb 16 21:09:47 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Feb 16 21:33:28 2014 +0100
@@ -673,8 +673,7 @@
         |> fold Int_Pair_Graph.add_deps_acyclic depss
         |> Int_Pair_Graph.topological_order
         handle Int_Pair_Graph.CYCLES _ =>
-               error "Cannot replay Metis proof in Isabelle without \
-                     \\"Hilbert_Choice\"."
+               error "Cannot replay Metis proof in Isabelle without \"Hilbert_Choice\""
       val ax_counts =
         Int_Tysubst_Table.empty
         |> fold (fn (ax_no, (_, (tysubst, _))) =>
@@ -732,7 +731,7 @@
                        THEN flexflex_tac)))
       handle ERROR msg =>
         cat_error msg
-          "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions."
+          "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions"
     end
 
 end;
diff -r 23d2cbac6dce -r 9429e7b5b827 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Sun Feb 16 21:09:47 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sun Feb 16 21:33:28 2014 +0100
@@ -283,7 +283,7 @@
 
 fun set_opt _ x NONE = SOME x
   | set_opt get x (SOME x0) =
-    error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^ ".")
+    error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x))
 
 fun consider_opt s =
   if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s])