# HG changeset patch
# User wenzelm
# Date 1440940885 -7200
# Node ID 3bc7dcc565dce3e0f893a9ed594e26ab1f90d59e
# Parent  0d401f8749422186c6028a82f8b2d48efc32ec83
clarified exceptions;
more careful treatment of missing context;

diff -r 0d401f874942 -r 3bc7dcc565dc src/Pure/context.ML
--- a/src/Pure/context.ML	Sun Aug 30 13:08:00 2015 +0200
+++ b/src/Pure/context.ML	Sun Aug 30 15:21:25 2015 +0200
@@ -451,7 +451,7 @@
 
 fun certificate_theory (Certificate thy) = thy
   | certificate_theory (Certificate_Id thy_id) =
-      raise Fail ("No content for theory certificate " ^ quote (display_name thy_id));
+      error ("No content for theory certificate " ^ quote (display_name thy_id));
 
 fun certificate_theory_id (Certificate thy) = theory_id thy
   | certificate_theory_id (Certificate_Id thy_id) = thy_id;
diff -r 0d401f874942 -r 3bc7dcc565dc src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Aug 30 13:08:00 2015 +0200
+++ b/src/Pure/display.ML	Sun Aug 30 15:21:25 2015 +0200
@@ -51,7 +51,7 @@
     val show_tags = Config.get ctxt show_tags;
     val show_hyps = Config.get ctxt show_hyps;
 
-    val th = Thm.strip_shyps raw_th;
+    val th = Thm.strip_shyps raw_th handle THM_CONTEXT _ => raw_th;
 
     val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th;
     val extra_shyps = Thm.extra_shyps th;
diff -r 0d401f874942 -r 3bc7dcc565dc src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Aug 30 13:08:00 2015 +0200
+++ b/src/Pure/thm.ML	Sun Aug 30 15:21:25 2015 +0200
@@ -198,6 +198,10 @@
 fun join_certificate0 (Cterm {cert = cert1, ...}, Cterm {cert = cert2, ...}) =
   Context.join_certificate (cert1, cert2);
 
+fun theory_of_cterm (ct as Cterm {cert, ...}) =
+  Context.certificate_theory cert
+    handle ERROR msg => raise CTERM_CONTEXT (msg, [ct], NONE);
+
 fun trim_context_cterm ct =
   (case ct of
     Cterm {cert = Context.Certificate_Id _, ...} => ct
@@ -328,7 +332,8 @@
      ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) =
   let
     val cert = join_certificate0 (ct1, ct2);
-    val thy = Context.certificate_theory cert;
+    val thy = Context.certificate_theory cert
+      handle ERROR msg => raise CTERM_CONTEXT (msg, [ct1, ct2], NONE);
     val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty);
     val sorts = Sorts.union sorts1 sorts2;
     fun mk_cTinst ((a, i), (S, T)) =
@@ -415,6 +420,7 @@
 val cert_of = #cert o rep_thm;
 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 ERROR msg => raise THM_CONTEXT (msg, [th], NONE);
@@ -517,7 +523,7 @@
 fun weaken_sorts raw_sorts ct =
   let
     val Cterm {cert, t, T, maxidx, sorts} = ct;
-    val thy = Context.certificate_theory cert;
+    val thy = theory_of_cterm ct;
     val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts);
     val sorts' = Sorts.union sorts more_sorts;
   in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;
@@ -625,7 +631,7 @@
     val Cterm {cert = cert, t = prop, T, maxidx, sorts} = ct;
     val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
 
-    val thy = Context.certificate_theory cert;
+    val thy = theory_of_cterm ct;
     val i = serial ();
     val future = future_thm |> Future.map (future_result i cert sorts prop);
   in