# HG changeset patch
# User wenzelm
# Date 1394719556 -3600
# Node ID f42de6d8ed8ed5a4247021ff122002bf935d4f56
# Parent  af71fb1cb31fb683bc03b9eeda61560cab1137d8
do not test details of error messages;

diff -r af71fb1cb31f -r f42de6d8ed8e src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Mar 13 12:28:35 2014 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Mar 13 15:05:56 2014 +0100
@@ -448,8 +448,8 @@
   by unfold_locales  (* subsumed, thm int2.assoc not generated *)
 
 ML {* (Global_Theory.get_thms @{theory} "int2.assoc";
-    error "thm int2.assoc was generated")
-  handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
+    raise Fail "thm int2.assoc was generated")
+  handle ERROR _ => ([]:thm list); *}
 
 thm int.lone int.right.rone
   (* the latter comes through the sublocale relation *)
@@ -782,8 +782,8 @@
 context container begin
 ML {* (Context.>> (fn generic => let val context = Context.proof_of generic
   val _ = Proof_Context.get_thms context "private.true" in generic end);
-  error "thm private.true was persisted")
-  handle ERROR "Unknown fact \"private.true\"" => ([]:thm list); *}
+  raise Fail "thm private.true was persisted")
+  handle ERROR _ => ([]:thm list); *}
 thm true_copy
 end