# HG changeset patch
# User wenzelm
# Date 1354896040 -3600
# Node ID 79858bd9f5ef731148cf5577150fea70c8619796
# Parent  eb7b59cc8e081424a3d91e65a61320d45c1079b3# Parent  7c8ce63a3c0021dbf09a588abd9356ac68284dda
merged

diff -r eb7b59cc8e08 -r 79858bd9f5ef src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Dec 07 16:38:25 2012 +0100
+++ b/src/HOL/Divides.thy	Fri Dec 07 17:00:40 2012 +0100
@@ -9,8 +9,6 @@
 imports Nat_Transfer
 begin
 
-ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
-
 subsection {* Syntactic division operations *}
 
 class div = dvd +
diff -r eb7b59cc8e08 -r 79858bd9f5ef src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Dec 07 16:38:25 2012 +0100
+++ b/src/HOL/List.thy	Fri Dec 07 17:00:40 2012 +0100
@@ -504,7 +504,228 @@
 *)
 
 
-ML_file "Tools/list_to_set_comprehension.ML"
+ML {*
+(* Simproc for rewriting list comprehensions applied to List.set to set
+   comprehension. *)
+
+signature LIST_TO_SET_COMPREHENSION =
+sig
+  val simproc : simpset -> cterm -> thm option
+end
+
+structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
+struct
+
+(* conversion *)
+
+fun all_exists_conv cv ctxt ct =
+  (case Thm.term_of ct of
+    Const (@{const_name HOL.Ex}, _) $ Abs _ =>
+      Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
+  | _ => cv ctxt ct)
+
+fun all_but_last_exists_conv cv ctxt ct =
+  (case Thm.term_of ct of
+    Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
+      Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
+  | _ => cv ctxt ct)
+
+fun Collect_conv cv ctxt ct =
+  (case Thm.term_of ct of
+    Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
+  | _ => raise CTERM ("Collect_conv", [ct]))
+
+fun Trueprop_conv cv ct =
+  (case Thm.term_of ct of
+    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
+  | _ => raise CTERM ("Trueprop_conv", [ct]))
+
+fun eq_conv cv1 cv2 ct =
+  (case Thm.term_of ct of
+    Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
+  | _ => raise CTERM ("eq_conv", [ct]))
+
+fun conj_conv cv1 cv2 ct =
+  (case Thm.term_of ct of
+    Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
+  | _ => raise CTERM ("conj_conv", [ct]))
+
+fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
+
+fun conjunct_assoc_conv ct =
+  Conv.try_conv
+    (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
+
+fun right_hand_set_comprehension_conv conv ctxt =
+  Trueprop_conv (eq_conv Conv.all_conv
+    (Collect_conv (all_exists_conv conv o #2) ctxt))
+
+
+(* term abstraction of list comprehension patterns *)
+
+datatype termlets = If | Case of (typ * int)
+
+fun simproc ss redex =
+  let
+    val ctxt = Simplifier.the_context ss
+    val thy = Proof_Context.theory_of ctxt
+    val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
+    val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
+    val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
+    val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
+    fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
+    fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
+    fun dest_singleton_list (Const (@{const_name List.Cons}, _)
+          $ t $ (Const (@{const_name List.Nil}, _))) = t
+      | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
+    (* We check that one case returns a singleton list and all other cases
+       return [], and return the index of the one singleton list case *)
+    fun possible_index_of_singleton_case cases =
+      let
+        fun check (i, case_t) s =
+          (case strip_abs_body case_t of
+            (Const (@{const_name List.Nil}, _)) => s
+          | _ => (case s of NONE => SOME i | SOME _ => NONE))
+      in
+        fold_index check cases NONE
+      end
+    (* returns (case_expr type index chosen_case) option  *)
+    fun dest_case case_term =
+      let
+        val (case_const, args) = strip_comb case_term
+      in
+        (case try dest_Const case_const of
+          SOME (c, T) =>
+            (case Datatype.info_of_case thy c of
+              SOME _ =>
+                (case possible_index_of_singleton_case (fst (split_last args)) of
+                  SOME i =>
+                    let
+                      val (Ts, _) = strip_type T
+                      val T' = List.last Ts
+                    in SOME (List.last args, T', i, nth args i) end
+                | NONE => NONE)
+            | NONE => NONE)
+        | NONE => NONE)
+      end
+    (* returns condition continuing term option *)
+    fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
+          SOME (cond, then_t)
+      | dest_if _ = NONE
+    fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
+      | tac ctxt (If :: cont) =
+          Splitter.split_tac [@{thm split_if}] 1
+          THEN rtac @{thm conjI} 1
+          THEN rtac @{thm impI} 1
+          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
+            CONVERSION (right_hand_set_comprehension_conv (K
+              (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
+               then_conv
+               rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
+          THEN tac ctxt cont
+          THEN rtac @{thm impI} 1
+          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
+              CONVERSION (right_hand_set_comprehension_conv (K
+                (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
+                 then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
+          THEN rtac set_Nil_I 1
+      | tac ctxt (Case (T, i) :: cont) =
+          let
+            val info = Datatype.the_info thy (fst (dest_Type T))
+          in
+            (* do case distinction *)
+            Splitter.split_tac [#split info] 1
+            THEN EVERY (map_index (fn (i', _) =>
+              (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
+              THEN REPEAT_DETERM (rtac @{thm allI} 1)
+              THEN rtac @{thm impI} 1
+              THEN (if i' = i then
+                (* continue recursively *)
+                Subgoal.FOCUS (fn {prems, context, ...} =>
+                  CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
+                      ((conj_conv
+                        (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
+                          (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
+                        Conv.all_conv)
+                        then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
+                        then_conv conjunct_assoc_conv)) context
+                    then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
+                      Conv.repeat_conv
+                        (all_but_last_exists_conv
+                          (K (rewr_conv'
+                            @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
+                THEN tac ctxt cont
+              else
+                Subgoal.FOCUS (fn {prems, context, ...} =>
+                  CONVERSION
+                    (right_hand_set_comprehension_conv (K
+                      (conj_conv
+                        ((eq_conv Conv.all_conv
+                          (rewr_conv' (List.last prems))) then_conv
+                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
+                        Conv.all_conv then_conv
+                        (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
+                      Trueprop_conv
+                        (eq_conv Conv.all_conv
+                          (Collect_conv (fn (_, ctxt) =>
+                            Conv.repeat_conv
+                              (Conv.bottom_conv
+                                (K (rewr_conv'
+                                  @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
+                THEN rtac set_Nil_I 1)) (#case_rewrites info))
+          end
+    fun make_inner_eqs bound_vs Tis eqs t =
+      (case dest_case t of
+        SOME (x, T, i, cont) =>
+          let
+            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
+            val x' = incr_boundvars (length vs) x
+            val eqs' = map (incr_boundvars (length vs)) eqs
+            val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
+            val constr_t =
+              list_comb
+                (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
+            val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
+          in
+            make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
+          end
+      | NONE =>
+          (case dest_if t of
+            SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
+          | NONE =>
+            if eqs = [] then NONE (* no rewriting, nothing to be done *)
+            else
+              let
+                val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
+                val pat_eq =
+                  (case try dest_singleton_list t of
+                    SOME t' =>
+                      Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
+                        Bound (length bound_vs) $ t'
+                  | NONE =>
+                      Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $
+                        Bound (length bound_vs) $ (mk_set rT $ t))
+                val reverse_bounds = curry subst_bounds
+                  ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
+                val eqs' = map reverse_bounds eqs
+                val pat_eq' = reverse_bounds pat_eq
+                val inner_t =
+                  fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
+                    (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
+                val lhs = term_of redex
+                val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
+                val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+              in
+                SOME
+                  ((Goal.prove ctxt [] [] rewrite_rule_t
+                    (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
+              end))
+  in
+    make_inner_eqs [] [] [] (dest_set (term_of redex))
+  end
+
+end
+*}
 
 simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
 
@@ -5664,7 +5885,57 @@
 
 subsubsection {* Pretty lists *}
 
-ML_file "Tools/list_code.ML"
+ML {*
+(* Code generation for list literals. *)
+
+signature LIST_CODE =
+sig
+  val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
+  val default_list: int * string
+    -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
+    -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
+  val add_literal_list: string -> theory -> theory
+end;
+
+structure List_Code : LIST_CODE =
+struct
+
+open Basic_Code_Thingol;
+
+fun implode_list nil' cons' t =
+  let
+    fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
+          if c = cons'
+          then SOME (t1, t2)
+          else NONE
+      | dest_cons _ = NONE;
+    val (ts, t') = Code_Thingol.unfoldr dest_cons t;
+  in case t'
+   of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
+    | _ => NONE
+  end;
+
+fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
+  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
+    pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
+    Code_Printer.str target_cons,
+    pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
+  );
+
+fun add_literal_list target =
+  let
+    fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
+      case Option.map (cons t1) (implode_list nil' cons' t2)
+       of SOME ts =>
+            Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
+        | NONE =>
+            default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
+  in Code_Target.add_const_syntax target @{const_name Cons}
+    (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
+  end
+
+end;
+*}
 
 code_type list
   (SML "_ list")
diff -r eb7b59cc8e08 -r 79858bd9f5ef src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Fri Dec 07 16:38:25 2012 +0100
+++ b/src/HOL/Nat_Transfer.thy	Fri Dec 07 17:00:40 2012 +0100
@@ -420,4 +420,8 @@
   return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   cong: setsum_cong setprod_cong]
 
+
+(*belongs to Divides.thy, but slows down dependency discovery*)
+ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
+
 end
diff -r eb7b59cc8e08 -r 79858bd9f5ef src/HOL/Tools/list_code.ML
--- a/src/HOL/Tools/list_code.ML	Fri Dec 07 16:38:25 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(*  Title:  HOL/Tools/list_code.ML
-    Author: Florian Haftmann, TU Muenchen
-
-Code generation for list literals.
-*)
-
-signature LIST_CODE =
-sig
-  val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
-  val default_list: int * string
-    -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
-    -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
-  val add_literal_list: string -> theory -> theory
-end;
-
-structure List_Code : LIST_CODE =
-struct
-
-open Basic_Code_Thingol;
-
-fun implode_list nil' cons' t =
-  let
-    fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
-          if c = cons'
-          then SOME (t1, t2)
-          else NONE
-      | dest_cons _ = NONE;
-    val (ts, t') = Code_Thingol.unfoldr dest_cons t;
-  in case t'
-   of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
-    | _ => NONE
-  end;
-
-fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
-  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
-    pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
-    Code_Printer.str target_cons,
-    pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
-  );
-
-fun add_literal_list target =
-  let
-    fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
-      case Option.map (cons t1) (implode_list nil' cons' t2)
-       of SOME ts =>
-            Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
-        | NONE =>
-            default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
-  in Code_Target.add_const_syntax target @{const_name Cons}
-    (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
-  end
-
-end;
diff -r eb7b59cc8e08 -r 79858bd9f5ef src/HOL/Tools/list_to_set_comprehension.ML
--- a/src/HOL/Tools/list_to_set_comprehension.ML	Fri Dec 07 16:38:25 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,224 +0,0 @@
-(*  Title:      HOL/Tools/list_to_set_comprehension.ML
-    Author:     Lukas Bulwahn, TU Muenchen
-
-Simproc for rewriting list comprehensions applied to List.set to set
-comprehension.
-*)
-
-signature LIST_TO_SET_COMPREHENSION =
-sig
-  val simproc : simpset -> cterm -> thm option
-end
-
-structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
-struct
-
-(* conversion *)
-
-fun all_exists_conv cv ctxt ct =
-  (case Thm.term_of ct of
-    Const (@{const_name HOL.Ex}, _) $ Abs _ =>
-      Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
-  | _ => cv ctxt ct)
-
-fun all_but_last_exists_conv cv ctxt ct =
-  (case Thm.term_of ct of
-    Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
-      Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
-  | _ => cv ctxt ct)
-
-fun Collect_conv cv ctxt ct =
-  (case Thm.term_of ct of
-    Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
-  | _ => raise CTERM ("Collect_conv", [ct]))
-
-fun Trueprop_conv cv ct =
-  (case Thm.term_of ct of
-    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
-  | _ => raise CTERM ("Trueprop_conv", [ct]))
-
-fun eq_conv cv1 cv2 ct =
-  (case Thm.term_of ct of
-    Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
-  | _ => raise CTERM ("eq_conv", [ct]))
-
-fun conj_conv cv1 cv2 ct =
-  (case Thm.term_of ct of
-    Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
-  | _ => raise CTERM ("conj_conv", [ct]))
-
-fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
-
-fun conjunct_assoc_conv ct =
-  Conv.try_conv
-    (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
-
-fun right_hand_set_comprehension_conv conv ctxt =
-  Trueprop_conv (eq_conv Conv.all_conv
-    (Collect_conv (all_exists_conv conv o #2) ctxt))
-
-
-(* term abstraction of list comprehension patterns *)
-
-datatype termlets = If | Case of (typ * int)
-
-fun simproc ss redex =
-  let
-    val ctxt = Simplifier.the_context ss
-    val thy = Proof_Context.theory_of ctxt
-    val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
-    val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
-    val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
-    val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
-    fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
-    fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
-    fun dest_singleton_list (Const (@{const_name List.Cons}, _)
-          $ t $ (Const (@{const_name List.Nil}, _))) = t
-      | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
-    (* We check that one case returns a singleton list and all other cases
-       return [], and return the index of the one singleton list case *)
-    fun possible_index_of_singleton_case cases =
-      let
-        fun check (i, case_t) s =
-          (case strip_abs_body case_t of
-            (Const (@{const_name List.Nil}, _)) => s
-          | _ => (case s of NONE => SOME i | SOME _ => NONE))
-      in
-        fold_index check cases NONE
-      end
-    (* returns (case_expr type index chosen_case) option  *)
-    fun dest_case case_term =
-      let
-        val (case_const, args) = strip_comb case_term
-      in
-        (case try dest_Const case_const of
-          SOME (c, T) =>
-            (case Datatype.info_of_case thy c of
-              SOME _ =>
-                (case possible_index_of_singleton_case (fst (split_last args)) of
-                  SOME i =>
-                    let
-                      val (Ts, _) = strip_type T
-                      val T' = List.last Ts
-                    in SOME (List.last args, T', i, nth args i) end
-                | NONE => NONE)
-            | NONE => NONE)
-        | NONE => NONE)
-      end
-    (* returns condition continuing term option *)
-    fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
-          SOME (cond, then_t)
-      | dest_if _ = NONE
-    fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
-      | tac ctxt (If :: cont) =
-          Splitter.split_tac [@{thm split_if}] 1
-          THEN rtac @{thm conjI} 1
-          THEN rtac @{thm impI} 1
-          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
-            CONVERSION (right_hand_set_comprehension_conv (K
-              (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
-               then_conv
-               rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
-          THEN tac ctxt cont
-          THEN rtac @{thm impI} 1
-          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
-              CONVERSION (right_hand_set_comprehension_conv (K
-                (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
-                 then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
-          THEN rtac set_Nil_I 1
-      | tac ctxt (Case (T, i) :: cont) =
-          let
-            val info = Datatype.the_info thy (fst (dest_Type T))
-          in
-            (* do case distinction *)
-            Splitter.split_tac [#split info] 1
-            THEN EVERY (map_index (fn (i', _) =>
-              (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
-              THEN REPEAT_DETERM (rtac @{thm allI} 1)
-              THEN rtac @{thm impI} 1
-              THEN (if i' = i then
-                (* continue recursively *)
-                Subgoal.FOCUS (fn {prems, context, ...} =>
-                  CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
-                      ((conj_conv
-                        (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
-                          (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
-                        Conv.all_conv)
-                        then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
-                        then_conv conjunct_assoc_conv)) context
-                    then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
-                      Conv.repeat_conv
-                        (all_but_last_exists_conv
-                          (K (rewr_conv'
-                            @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
-                THEN tac ctxt cont
-              else
-                Subgoal.FOCUS (fn {prems, context, ...} =>
-                  CONVERSION
-                    (right_hand_set_comprehension_conv (K
-                      (conj_conv
-                        ((eq_conv Conv.all_conv
-                          (rewr_conv' (List.last prems))) then_conv
-                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
-                        Conv.all_conv then_conv
-                        (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
-                      Trueprop_conv
-                        (eq_conv Conv.all_conv
-                          (Collect_conv (fn (_, ctxt) =>
-                            Conv.repeat_conv
-                              (Conv.bottom_conv
-                                (K (rewr_conv'
-                                  @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
-                THEN rtac set_Nil_I 1)) (#case_rewrites info))
-          end
-    fun make_inner_eqs bound_vs Tis eqs t =
-      (case dest_case t of
-        SOME (x, T, i, cont) =>
-          let
-            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
-            val x' = incr_boundvars (length vs) x
-            val eqs' = map (incr_boundvars (length vs)) eqs
-            val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
-            val constr_t =
-              list_comb
-                (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
-            val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
-          in
-            make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
-          end
-      | NONE =>
-          (case dest_if t of
-            SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
-          | NONE =>
-            if eqs = [] then NONE (* no rewriting, nothing to be done *)
-            else
-              let
-                val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
-                val pat_eq =
-                  (case try dest_singleton_list t of
-                    SOME t' =>
-                      Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
-                        Bound (length bound_vs) $ t'
-                  | NONE =>
-                      Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $
-                        Bound (length bound_vs) $ (mk_set rT $ t))
-                val reverse_bounds = curry subst_bounds
-                  ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
-                val eqs' = map reverse_bounds eqs
-                val pat_eq' = reverse_bounds pat_eq
-                val inner_t =
-                  fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
-                    (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
-                val lhs = term_of redex
-                val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
-                val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-              in
-                SOME
-                  ((Goal.prove ctxt [] [] rewrite_rule_t
-                    (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
-              end))
-  in
-    make_inner_eqs [] [] [] (dest_set (term_of redex))
-  end
-
-end
diff -r eb7b59cc8e08 -r 79858bd9f5ef src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Pure/General/exn.scala	Fri Dec 07 17:00:40 2012 +0100
@@ -45,5 +45,23 @@
 
   def message(exn: Throwable): String =
     user_message(exn) getOrElse exn.toString
+
+
+  /* recover from spurious crash */
+
+  def recover[A](e: => A): A =
+  {
+    capture(e) match {
+      case Res(x) => x
+      case Exn(exn) =>
+        capture(e) match {
+          case Res(x) =>
+            java.lang.System.err.println("Recovered from spurious crash after retry!")
+            exn.printStackTrace()
+            x
+          case Exn(_) => throw exn
+        }
+    }
+  }
 }
 
diff -r eb7b59cc8e08 -r 79858bd9f5ef src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Pure/System/build.scala	Fri Dec 07 17:00:40 2012 +0100
@@ -376,9 +376,10 @@
           val syntax = thy_deps.make_syntax
 
           val all_files =
-            (thy_deps.deps.map({ case (n, h) =>
-              val thy = Path.explode(n.node)
-              val uses = h.uses.map(p => Path.explode(n.dir) + Path.explode(p._1))
+            (thy_deps.deps.map({ case dep =>
+              val thy = Path.explode(dep.name.node)
+              val uses = dep.join_header.uses.map(p =>
+                Path.explode(dep.name.dir) + Path.explode(p._1))
               thy :: uses
             }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
 
@@ -392,7 +393,7 @@
                 error(msg + "\nThe error(s) above occurred in session " +
                   quote(name) + Position.here(info.pos))
             }
-          val errors = parent_errors ::: thy_deps.deps.map(d => d._2.errors).flatten
+          val errors = parent_errors ::: thy_deps.deps.map(dep => dep.join_header.errors).flatten
 
           deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
       }))
diff -r eb7b59cc8e08 -r 79858bd9f5ef src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Pure/Thy/thy_info.scala	Fri Dec 07 17:00:40 2012 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import java.util.concurrent.{Future => JFuture}
+
+
 class Thy_Info(thy_load: Thy_Load)
 {
   /* messages */
@@ -24,7 +27,13 @@
 
   /* dependencies */
 
-  type Dep = (Document.Node.Name, Document.Node.Header)
+  sealed case class Dep(
+    name: Document.Node.Name,
+    header0: Document.Node.Header,
+    future_header: JFuture[Exn.Result[Document.Node.Header]])
+  {
+    def join_header: Document.Node.Header = Exn.release(future_header.get)
+  }
 
   object Dependencies
   {
@@ -37,7 +46,7 @@
     val seen: Set[Document.Node.Name])
   {
     def :: (dep: Dep): Dependencies =
-      new Dependencies(dep :: rev_deps, dep._2.keywords ::: keywords, seen)
+      new Dependencies(dep :: rev_deps, dep.header0.keywords ::: keywords, seen)
 
     def + (name: Document.Node.Name): Dependencies =
       new Dependencies(rev_deps, keywords, seen = seen + name)
@@ -45,7 +54,7 @@
     def deps: List[Dep] = rev_deps.reverse
 
     def loaded_theories: Set[String] =
-      (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory }
+      (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
 
     def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
   }
@@ -60,24 +69,48 @@
     if (required.seen(name)) required
     else if (thy_load.loaded_theories(name.theory)) required + name
     else {
+      def err(msg: String): Nothing =
+        cat_error(msg, "The error(s) above occurred while examining theory " +
+          quote(name.theory) + required_by(initiators))
+
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
         val syntax = required.make_syntax
-        val header =
-          try {
-            if (files) thy_load.check_thy_files(syntax, name)
-            else thy_load.check_thy(name)
+
+        val header0 =
+          try { thy_load.check_thy(name) }
+          catch { case ERROR(msg) => err(msg) }
+
+        val future_header: JFuture[Exn.Result[Document.Node.Header]] =
+          if (files) {
+            val string = thy_load.with_thy_text(name, _.toString)
+            val syntax0 = syntax.add_keywords(header0.keywords)
+
+            if (thy_load.body_files_test(syntax0, string)) {
+              /* FIXME
+                  unstable in scala-2.9.2 on multicore hardware -- spurious NPE
+                  OK in scala-2.10.0.RC3 */
+              // default_thread_pool.submit(() =>
+                Library.future_value(Exn.capture {
+                  try {
+                    val files = thy_load.body_files(syntax0, string)
+                    header0.copy(uses = header0.uses ::: files.map((_, false)))
+                  }
+                  catch { case ERROR(msg) => err(msg) }
+                })
+              //)
+            }
+            else Library.future_value(Exn.Res(header0))
           }
-          catch {
-            case ERROR(msg) =>
-              cat_error(msg, "The error(s) above occurred while examining theory " +
-                quote(name.theory) + required_by(initiators))
-          }
-        (name, header) :: require_thys(files, name :: initiators, required + name, header.imports)
+          else Library.future_value(Exn.Res(header0))
+
+        Dep(name, header0, future_header) ::
+          require_thys(files, name :: initiators, required + name, header0.imports)
       }
       catch {
         case e: Throwable =>
-          (name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
+          val bad_header = Document.Node.bad_header(Exn.message(e))
+          Dep(name, bad_header, Library.future_value(Exn.Res(bad_header))) :: (required + name)
       }
     }
   }
diff -r eb7b59cc8e08 -r 79858bd9f5ef src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Fri Dec 07 17:00:40 2012 +0100
@@ -80,53 +80,47 @@
     clean_tokens.reverse.find(_.is_name).map(_.content)
   }
 
-  def find_files(syntax: Outer_Syntax, text: String): List[String] =
+  def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
+    syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+
+  def body_files(syntax: Outer_Syntax, text: String): List[String] =
   {
     val thy_load_commands = syntax.thy_load_commands
-    if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
-      val spans = Thy_Syntax.parse_spans(syntax.scan(text))
-      spans.iterator.map({
-        case toks @ (tok :: _) if tok.is_command =>
-          thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
-            case Some((_, exts)) =>
-              find_file(toks) match {
-                case Some(file) =>
-                  if (exts.isEmpty) List(file)
-                  else exts.map(ext => file + "." + ext)
-                case None => Nil
-              }
-            case None => Nil
-          }
-        case _ => Nil
-      }).flatten.toList
-    }
-    else Nil
+    val spans = Thy_Syntax.parse_spans(syntax.scan(text))
+    spans.iterator.map({
+      case toks @ (tok :: _) if tok.is_command =>
+        thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
+          case Some((_, exts)) =>
+            find_file(toks) match {
+              case Some(file) =>
+                if (exts.isEmpty) List(file)
+                else exts.map(ext => file + "." + ext)
+              case None => Nil
+            }
+          case None => Nil
+        }
+      case _ => Nil
+    }).flatten.toList
   }
 
   def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
   {
-    val header = Thy_Header.read(text)
+    try {
+      val header = Thy_Header.read(text)
 
-    val name1 = header.name
-    if (name.theory != name1)
-      error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
-        " for theory " + quote(name1))
+      val name1 = header.name
+      if (name.theory != name1)
+        error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
+          " for theory " + quote(name1))
 
-    val imports = header.imports.map(import_name(name.dir, _))
-    val uses = header.uses
-    Document.Node.Header(imports, header.keywords, uses)
+      val imports = header.imports.map(import_name(name.dir, _))
+      val uses = header.uses
+      Document.Node.Header(imports, header.keywords, uses)
+    }
+    catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) }
   }
 
   def check_thy(name: Document.Node.Name): Document.Node.Header =
     with_thy_text(name, check_thy_text(name, _))
-
-  def check_thy_files(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header =
-    with_thy_text(name, text =>
-      {
-        val string = text.toString
-        val header = check_thy_text(name, string)
-        val more_uses = find_files(syntax.add_keywords(header.keywords), string)
-        header.copy(uses = header.uses ::: more_uses.map((_, false)))
-      })
 }
 
diff -r eb7b59cc8e08 -r 79858bd9f5ef src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Pure/library.scala	Fri Dec 07 17:00:40 2012 +0100
@@ -10,6 +10,7 @@
 
 import java.lang.System
 import java.util.Locale
+import java.util.concurrent.{Future => JFuture, TimeUnit}
 import java.awt.Component
 import javax.swing.JOptionPane
 
@@ -187,6 +188,18 @@
     selection.index = 3
     prototypeDisplayValue = Some("00000%")
   }
+
+
+  /* Java futures */
+
+  def future_value[A](x: A) = new JFuture[A]
+  {
+    def cancel(may_interrupt: Boolean): Boolean = false
+    def isCancelled(): Boolean = false
+    def isDone(): Boolean = true
+    def get(): A = x
+    def get(timeout: Long, time_unit: TimeUnit): A = x
+  }
 }
 
 
diff -r eb7b59cc8e08 -r 79858bd9f5ef src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Dec 07 17:00:40 2012 +0100
@@ -316,21 +316,18 @@
 fi
 
 
-# build logic
-
-if [ "$NO_BUILD" = false ]; then
-  "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -L jedit_logic "$JEDIT_LOGIC"
-  RC="$?"
-  [ "$RC" = 0 ] || exit "$RC"
-fi
-
-
 # main
 
-[ "$BUILD_ONLY" = true ] || {
+if [ "$BUILD_ONLY" = false ]; then
+  if [ "$NO_BUILD" = false ]; then
+    "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -L jedit_logic "$JEDIT_LOGIC"
+    RC="$?"
+    [ "$RC" = 0 ] || exit "$RC"
+  fi
+
   export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
 
   exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
     -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
     "-settings=$(jvmpath "$JEDIT_SETTINGS")" "${ARGS[@]}"
-}
+fi
diff -r eb7b59cc8e08 -r 79858bd9f5ef src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Dec 07 17:00:40 2012 +0100
@@ -157,7 +157,7 @@
 
         val thy_info = new Thy_Info(PIDE.thy_load)
         // FIXME avoid I/O in Swing thread!?!
-        val files = thy_info.dependencies(true, thys).deps.map(_._1.node).
+        val files = thy_info.dependencies(true, thys).deps.map(_.name.node).
           filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
 
         if (!files.isEmpty) {