# HG changeset patch
# User wenzelm
# Date 1440798483 -7200
# Node ID c7a7f063704af44a37613a48304dfa20f62f78c7
# Parent  b7af255dd20008b32cd80e23e4bfaeb89752a021
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);

diff -r b7af255dd200 -r c7a7f063704a src/Pure/context.ML
--- a/src/Pure/context.ML	Fri Aug 28 23:21:04 2015 +0200
+++ b/src/Pure/context.ML	Fri Aug 28 23:48:03 2015 +0200
@@ -466,7 +466,7 @@
     else if proper_subthy_id (thy_id2, thy_id1) then cert1
     else if proper_subthy_id (thy_id1, thy_id2) then cert2
     else
-      raise Fail ("Cannot join unrelated theory certificates " ^
+      error ("Cannot join unrelated theory certificates " ^
         quote (display_name thy_id1) ^ " and " ^ quote (display_name thy_id2))
   end;
 
diff -r b7af255dd200 -r c7a7f063704a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Aug 28 23:21:04 2015 +0200
+++ b/src/Pure/thm.ML	Fri Aug 28 23:48:03 2015 +0200
@@ -15,6 +15,7 @@
   type thm
   type conv = cterm -> thm
   exception THM of string * int * thm list
+  exception THM_CONTEXT of string * thm list * Proof.context option
 end;
 
 signature THM =
@@ -356,6 +357,7 @@
 
 (*errors involving theorems*)
 exception THM of string * int * thm list;
+exception THM_CONTEXT of string * thm list * Proof.context option;
 
 fun rep_thm (Thm (_, args)) = args;
 
@@ -403,7 +405,8 @@
 val theory_id_of_thm = Context.certificate_theory_id o cert_of;
 val theory_name_of_thm = Context.theory_id_name o theory_id_of_thm;
 fun theory_of_thm th =
-  Context.certificate_theory (cert_of th) handle Fail msg => raise THM (msg, 0, [th]);
+  Context.certificate_theory (cert_of th)
+    handle ERROR msg => raise THM_CONTEXT (msg, [th], NONE);
 
 val maxidx_of = #maxidx o rep_thm;
 fun maxidx_thm th i = Int.max (maxidx_of th, i);
@@ -462,14 +465,14 @@
 
 fun make_context ths NONE cert =
       (Context.Theory (Context.certificate_theory cert)
-        handle Fail msg => raise THM (msg, 0, ths))
-  | make_context _ (SOME ctxt) cert =
+        handle ERROR msg => raise THM_CONTEXT (msg, ths, NONE))
+  | make_context ths (SOME ctxt) cert =
       let
         val thy_id = Context.certificate_theory_id cert;
         val thy_id' = Context.theory_id (Proof_Context.theory_of ctxt);
       in
         if Context.subthy_id (thy_id, thy_id') then Context.Proof ctxt
-        else raise THEORY ("Bad context", [Proof_Context.theory_of ctxt])
+        else raise THM_CONTEXT ("Bad context", ths, SOME ctxt)
       end;
 
 (*explicit weakening: maps |- B to A |- B*)