--- 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)
--- 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;
--- 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])