# HG changeset patch
# User wenzelm
# Date 1231547311 -3600
# Node ID 6baa02c8263e687a37fc1e24c90b8d6680d2b083
# Parent  948d616959e4dc19fe34a0fe1f59f77583ad4d1e# Parent  75ac4d6ff8fb64e9aa74779845ee64b767070060
merged

diff -r 948d616959e4 -r 6baa02c8263e src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -571,7 +571,7 @@
         InductivePackage.add_inductive_global (serial_string ())
           {quiet_mode = false, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
-           skip_mono = true}
+           skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
              (rep_set_names' ~~ recTs'))
           [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
@@ -1509,7 +1509,7 @@
         InductivePackage.add_inductive_global (serial_string ())
           {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
-           skip_mono = true}
+           skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
           (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
diff -r 948d616959e4 -r 6baa02c8263e src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -155,7 +155,7 @@
         InductivePackage.add_inductive_global (serial_string ())
           {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
             alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
-            skip_mono = true}
+            skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
           (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
diff -r 948d616959e4 -r 6baa02c8263e src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -183,7 +183,7 @@
         InductivePackage.add_inductive_global (serial_string ())
           {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
-           skip_mono = true}
+           skip_mono = true, fork_mono = false}
           (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
           (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1;
 
diff -r 948d616959e4 -r 6baa02c8263e src/HOL/Tools/function_package/inductive_wrap.ML
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -48,7 +48,8 @@
               coind = false,
               no_elim = false,
               no_ind = false,
-              skip_mono = true}
+              skip_mono = true,
+              fork_mono = false}
             [((Binding.name R, T), NoSyn)] (* the relation *)
             [] (* no parameters *)
             (map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *)
diff -r 948d616959e4 -r 6baa02c8263e src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -46,7 +46,7 @@
     (Binding.T * string option * mixfix) list ->
     (Attrib.binding * string) list ->
     (Facts.ref * Attrib.src list) list ->
-    local_theory -> inductive_result * local_theory
+    bool -> local_theory -> inductive_result * local_theory
   val add_inductive_global: string -> inductive_flags ->
     ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
     thm list -> theory -> inductive_result * theory
@@ -74,9 +74,9 @@
     (Binding.T * string option * mixfix) list ->
     (Binding.T * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
-    local_theory -> inductive_result * local_theory
+    bool -> local_theory -> inductive_result * local_theory
   val gen_ind_decl: add_ind_def -> bool ->
-    OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list
+    OuterParse.token list -> (bool -> local_theory -> local_theory) * OuterParse.token list
 end;
 
 structure InductivePackage: INDUCTIVE_PACKAGE =
@@ -312,10 +312,11 @@
 
 (* prove monotonicity *)
 
-fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
- (message (quiet_mode orelse skip_mono andalso !quick_and_dirty)
+fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
+ (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
     "  Proving monotonicity ...";
-  (if skip_mono then SkipProof.prove else Goal.prove) ctxt [] []
+  (if skip_mono then SkipProof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
+    [] []
     (HOLogic.mk_Trueprop
       (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
     (fn _ => EVERY [rtac @{thm monoI} 1,
@@ -582,7 +583,7 @@
 
 (** specification of (co)inductive predicates **)
 
-fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
+fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
   let
     val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
 
@@ -662,9 +663,11 @@
     val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
-    val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt''
+    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt'';
+    val ((_, [mono']), ctxt''') =
+      LocalTheory.note Thm.internalK (Attrib.empty_binding, [mono]) ctxt'';
 
-  in (ctxt'', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
+  in (ctxt''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
     list_comb (rec_const, params), preds, argTs, bs, xs)
   end;
 
@@ -718,7 +721,7 @@
 
 type inductive_flags =
   {quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T,
-   coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool}
+   coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
 
 type add_ind_def =
   inductive_flags ->
@@ -726,7 +729,7 @@
   term list -> (Binding.T * mixfix) list ->
   local_theory -> inductive_result * local_theory
 
-fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
+fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     cs intros monos params cnames_syn ctxt =
   let
     val _ = null cnames_syn andalso error "No inductive predicates given";
@@ -739,7 +742,7 @@
       apfst split_list (split_list (map (check_rule ctxt cs params) intros));
 
     val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
-      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
+      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
         monos params cnames_syn ctxt;
 
     val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
@@ -780,7 +783,7 @@
 (* external interfaces *)
 
 fun gen_add_inductive_i mk_def
-    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono})
+    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
     cnames_syn pnames spec monos lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -836,7 +839,7 @@
     ||> fold (snd oo LocalTheory.abbrev Syntax.mode_default) abbrevs
   end;
 
-fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
+fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
   let
     val ((vars, specs), _) = lthy |> ProofContext.set_mode ProofContext.mode_abbrev
       |> Specification.read_specification
@@ -845,7 +848,8 @@
     val intrs = map (apsnd the_single) specs;
     val monos = Attrib.eval_thms lthy raw_monos;
     val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
-      alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false, skip_mono = false};
+      alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
+      skip_mono = false, fork_mono = not int};
   in
     lthy
     |> LocalTheory.set_group (serial_string ())
@@ -956,12 +960,12 @@
   Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] --
   Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
   >> (fn (((preds, params), specs), monos) =>
-      (snd o gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
+      (snd oo gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
 
 val ind_decl = gen_ind_decl add_ind_def;
 
-val _ = OuterSyntax.local_theory "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
-val _ = OuterSyntax.local_theory "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
+val _ = OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
+val _ = OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
 
 val _ =
   OuterSyntax.local_theory "inductive_cases"
diff -r 948d616959e4 -r 6baa02c8263e src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -347,7 +347,7 @@
     val (ind_info, thy3') = thy2 |>
       InductivePackage.add_inductive_global (serial_string ())
         {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
-          coind = false, no_elim = false, no_ind = false, skip_mono = false}
+          coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Binding.name (Sign.base_name (name_of_thm intr)), []),
            subst_atomic rlzpreds' (Logic.unvarify rintr)))
diff -r 948d616959e4 -r 6baa02c8263e src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -20,7 +20,7 @@
     (Binding.T * string option * mixfix) list ->
     (Binding.T * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
-    local_theory -> InductivePackage.inductive_result * local_theory
+    bool -> local_theory -> InductivePackage.inductive_result * local_theory
   val codegen_preproc: theory -> thm list -> thm list
   val setup: theory -> theory
 end;
@@ -403,7 +403,8 @@
 
 (**** definition of inductive sets ****)
 
-fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
+fun add_ind_set_def
+    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     cs intros monos params cnames_syn ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
@@ -468,7 +469,8 @@
     val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
       InductivePackage.add_ind_def
         {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
-          coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
+          coind = coind, no_elim = no_elim, no_ind = no_ind,
+          skip_mono = skip_mono, fork_mono = fork_mono}
         cs' intros' monos' params1 cnames_syn' ctxt;
 
     (* define inductive sets using previously defined predicates *)
@@ -550,10 +552,10 @@
 val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
 
 val _ =
-  OuterSyntax.local_theory "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
+  OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
 
 val _ =
-  OuterSyntax.local_theory "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
+  OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
 
 end;
 
diff -r 948d616959e4 -r 6baa02c8263e src/Pure/General/lazy.ML
--- a/src/Pure/General/lazy.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/General/lazy.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/lazy.ML
-    ID:         $Id$
     Author:     Florian Haftmann and Makarius, TU Muenchen
 
 Lazy evaluation with memoing.  Concurrency may lead to multiple
@@ -13,6 +12,7 @@
   val lazy: (unit -> 'a) -> 'a lazy
   val value: 'a -> 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
+  val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
   val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
 end
@@ -41,7 +41,7 @@
 
 (* force result *)
 
-fun force r =
+fun force_result r =
   let
     (*potentially concurrent evaluation*)
     val res =
@@ -53,7 +53,9 @@
       (case ! r of
         Lazy _ => (r := Result res; res)
       | Result res' => res'));
-  in Exn.release res' end;
+  in res' end;
+
+fun force r = Exn.release (force_result r);
 
 fun map_force f = value o f o force;
 
diff -r 948d616959e4 -r 6baa02c8263e src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/General/markup.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -85,8 +85,9 @@
   val subgoalN: string val subgoal: T
   val sendbackN: string val sendback: T
   val hiliteN: string val hilite: T
+  val taskN: string
   val unprocessedN: string val unprocessed: T
-  val runningN: string val running: T
+  val runningN: string val running: string -> T
   val failedN: string val failed: T
   val finishedN: string val finished: T
   val disposedN: string val disposed: T
@@ -259,8 +260,10 @@
 
 (* command status *)
 
+val taskN = "task";
+
 val (unprocessedN, unprocessed) = markup_elem "unprocessed";
-val (runningN, running) = markup_elem "running";
+val (runningN, running) = markup_string "running" taskN;
 val (failedN, failed) = markup_elem "failed";
 val (finishedN, finished) = markup_elem "finished";
 val (disposedN, disposed) = markup_elem "disposed";
diff -r 948d616959e4 -r 6baa02c8263e src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/General/markup.scala	Sat Jan 10 01:28:31 2009 +0100
@@ -110,6 +110,8 @@
 
   /* command status */
 
+  val TASK = "task"
+
   val UNPROCESSED = "unprocessed"
   val RUNNING = "running"
   val FAILED = "failed"
diff -r 948d616959e4 -r 6baa02c8263e src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/Isar/isar.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -194,7 +194,7 @@
   Finished of Toplevel.state;
 
 fun status_markup Unprocessed = Markup.unprocessed
-  | status_markup Running = Markup.running
+  | status_markup Running = (Markup.runningN, [])
   | status_markup (Failed _) = Markup.failed
   | status_markup (Finished _) = Markup.finished;
 
diff -r 948d616959e4 -r 6baa02c8263e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -345,7 +345,8 @@
       (case filter_out (fn s => s = "") strs of [] => ""
       | strs' => enclose " (" ")" (commas strs'));
 
-    fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
+    fun prt_goal (SOME (ctxt, (i,
+      {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
           pretty_facts "using " ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Pretty.str ("goal" ^
diff -r 948d616959e4 -r 6baa02c8263e src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Thy/thy_info.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Main part of theory loader database, including handling of theory and
@@ -24,6 +23,8 @@
   val get_parents: string -> string list
   val touch_thy: string -> unit
   val touch_child_thys: string -> unit
+  val remove_thy: string -> unit
+  val kill_thy: string -> unit
   val provide_file: Path.T -> string -> unit
   val load_file: bool -> Path.T -> unit
   val exec_file: bool -> Path.T -> Context.generic -> Context.generic
@@ -32,8 +33,6 @@
   val use_thys: string list -> unit
   val use_thy: string -> unit
   val time_use_thy: string -> unit
-  val remove_thy: string -> unit
-  val kill_thy: string -> unit
   val thy_ord: theory * theory -> order
   val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
   val end_theory: theory -> unit
@@ -232,6 +231,27 @@
 end;
 
 
+(* remove theory *)
+
+fun remove_thy name =
+  if is_finished name then error (loader_msg "cannot remove finished theory" [name])
+  else
+    let val succs = thy_graph Graph.all_succs [name] in
+      priority (loader_msg "removing" succs);
+      CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)))
+    end;
+
+val kill_thy = if_known_thy remove_thy;
+
+fun consolidate_thy name =
+  (case lookup_theory name of
+    NONE => []
+  | SOME thy =>
+      (case PureThy.join_proofs thy of
+        [] => []
+      | exns => (kill_thy name; exns)));
+
+
 (* load_file *)
 
 local
@@ -342,7 +362,7 @@
       in (x, Symtab.update (name, x) tab) end;
 
     val thy_results = Future.join_results (#1 (fold_map future tasks Symtab.empty));
-    val proof_results = PureThy.join_proofs (map_filter (try get_theory o #1) tasks);
+    val proof_results = map Exn.Exn (maps (consolidate_thy o #1) tasks);
   in ignore (Exn.release_all (thy_results @ proof_results)) end;
 
 in
@@ -464,19 +484,6 @@
 end;
 
 
-(* remove theory *)
-
-fun remove_thy name =
-  if is_finished name then error (loader_msg "cannot remove finished theory" [name])
-  else
-    let val succs = thy_graph Graph.all_succs [name] in
-      priority (loader_msg "removing" succs);
-      CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)))
-    end;
-
-val kill_thy = if_known_thy remove_thy;
-
-
 (* update_time *)
 
 structure UpdateTime = TheoryDataFun
diff -r 948d616959e4 -r 6baa02c8263e src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Thy/thy_load.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Theory loader primitives, including load path.
@@ -22,6 +21,7 @@
   val ml_exts: string list
   val ml_path: string -> Path.T
   val thy_path: string -> Path.T
+  val split_thy_path: Path.T -> Path.T * string
   val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_thy: Path.T -> string -> Path.T * File.ident
@@ -62,6 +62,11 @@
 val ml_path = Path.ext "ML" o Path.basic;
 val thy_path = Path.ext "thy" o Path.basic;
 
+fun split_thy_path path =
+  (case Path.split_ext path of
+    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
+  | _ => error ("Bad theory file specification " ^ Path.implode path));
+
 
 (* check files *)
 
diff -r 948d616959e4 -r 6baa02c8263e src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/pure_thy.ML	Sat Jan 10 01:28:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/pure_thy.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Theorem storage.  Pure theory syntax and logical content.
@@ -11,7 +10,7 @@
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
   val hide_fact: bool -> string -> theory -> theory
-  val join_proofs: theory list -> unit Exn.result list
+  val join_proofs: theory -> exn list
   val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
@@ -81,7 +80,8 @@
 
 fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
 
-val join_proofs = maps (fn thy => map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy))));
+fun join_proofs thy =
+  map_filter (Exn.get_exn o Lazy.force_result) (rev (#2 (FactsData.get thy)));