--- 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