Improve exception messages out of THEN1

HOL-Theorem-Prover · Jul 15, 2022 · 6e4bd2f · 6e4bd2f
1 parent 47d94ba
commit 6e4bd2f
Showing 1 changed file with 6 additions and 3 deletions.
diff --git a/src/1/Tactical.sml b/src/1/Tactical.sml
@@ -225,9 +225,12 @@ val op >- = op THEN1
 fun op>>-(tac1, n) tac2 g =
   op>- (tac1, tac2) g
   handle e as HOL_ERR {message,origin_structure,origin_function} =>
-    raise HOL_ERR {message = message ^ " (THEN1 on line "^Int.toString n^")",
-                   origin_function = origin_function,
-                   origin_structure = origin_structure}
+         if is_substring "THEN1" message then raise e
+         else
+           raise HOL_ERR {message = message ^
+                                    " (THEN1 on line "^Int.toString n^")",
+                          origin_function = origin_function,
+                          origin_structure = origin_structure}
 fun (f ?? x) = f x