# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1519119243 0
# Node ID 738f170f43ee4977ea138b3224c0b1a50e1bc1a4
# Parent  67909bfc392340d9311467e00288130d718f325f# Parent  52b0d4cd4be7a7f2b660f2ee95338b0908cfef8c
Merge

diff -r 67909bfc3923 -r 738f170f43ee src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/Function/function_common.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -276,8 +276,7 @@
 
 fun retrieve_function_data ctxt t =
   Item_Net.retrieve (get_functions ctxt) t
-  |> (map o apsnd)
-      (transform_function_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
+  |> (map o apsnd) (transform_function_data (Morphism.transfer_morphism' ctxt));
 
 val add_function_data =
   transform_function_data Morphism.trim_context_morphism #>
diff -r 67909bfc3923 -r 738f170f43ee src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -60,7 +60,7 @@
 
 fun lookup_mode ctxt =
   Symtab.lookup (Modes.get (Context.Proof ctxt))
-  #> Option.map (transform_setup_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
+  #> Option.map (transform_setup_data (Morphism.transfer_morphism' ctxt));
 
 
 (*** Automated monotonicity proofs ***)
diff -r 67909bfc3923 -r 738f170f43ee src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -106,7 +106,7 @@
 
 fun lookup_quotmaps_generic context name =
   Symtab.lookup (get_quotmaps context) name
-  |> Option.map (transform_quotmaps (Morphism.transfer_morphism (Context.theory_of context)))
+  |> Option.map (transform_quotmaps (Morphism.transfer_morphism'' context))
 
 val lookup_quotmaps = lookup_quotmaps_generic o Context.Proof
 val lookup_quotmaps_global = lookup_quotmaps_generic o Context.Theory
@@ -172,7 +172,7 @@
 
 fun lookup_quotients_generic context name =
   Symtab.lookup (get_quotients context) name
-  |> Option.map (transform_quotients (Morphism.transfer_morphism (Context.theory_of context)))
+  |> Option.map (transform_quotients (Morphism.transfer_morphism'' context))
 
 val lookup_quotients = lookup_quotients_generic o Context.Proof
 val lookup_quotients_global = lookup_quotients_generic o Context.Theory
@@ -211,7 +211,7 @@
 
 fun dest_quotconsts_generic context =
   maps #2 (Symtab.dest (get_quotconsts context))
-  |> map (transform_quotconsts (Morphism.transfer_morphism (Context.theory_of context)))
+  |> map (transform_quotconsts (Morphism.transfer_morphism'' context))
 
 val dest_quotconsts = dest_quotconsts_generic o Context.Proof
 val dest_quotconsts_global = dest_quotconsts_generic o Context.Theory
diff -r 67909bfc3923 -r 738f170f43ee src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -868,7 +868,7 @@
   end
 
 fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
-  |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
+  |> Option.map (morph_pred_data (Morphism.transfer_morphism' ctxt))
 
 fun update_pred_data type_name qinfo ctxt =
   Data.map (map_pred_data (Symtab.update (type_name, qinfo))) ctxt
diff -r 67909bfc3923 -r 738f170f43ee src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/inductive.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -257,14 +257,14 @@
 fun the_inductive ctxt term =
   Item_Net.retrieve (#infos (rep_data ctxt)) term
   |> the_single
-  |> apsnd (transform_result (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
+  |> apsnd (transform_result (Morphism.transfer_morphism' ctxt))
 
 fun the_inductive_global ctxt name =
   #infos (rep_data ctxt)
   |> Item_Net.content
   |> filter (fn ({names, ...}, _) => member op = names name)
   |> the_single
-  |> apsnd (transform_result (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
+  |> apsnd (transform_result (Morphism.transfer_morphism' ctxt))
 
 fun put_inductives info =
   map_data (fn (infos, monos, equations) =>
diff -r 67909bfc3923 -r 738f170f43ee src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/typedef.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -72,7 +72,7 @@
 
 fun get_info_generic context =
   Symtab.lookup_list (Data.get context) #>
-  map (transform_info (Morphism.transfer_morphism (Context.theory_of context)));
+  map (transform_info (Morphism.transfer_morphism'' context));
 
 val get_info = get_info_generic o Context.Proof;
 val get_info_global = get_info_generic o Context.Theory;
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Concurrent/future.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -31,6 +31,8 @@
   val join_result: 'a future -> 'a Exn.result
   val joins: 'a future list -> 'a list
   val join: 'a future -> 'a
+  val forked_results: {name: string, deps: Task_Queue.task list} ->
+    (unit -> 'a) list -> 'a Exn.result list
   val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
@@ -539,6 +541,24 @@
 fun join x = Exn.release (join_result x);
 
 
+(* forked results: nested parallel evaluation *)
+
+fun forked_results {name, deps} es =
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+    let
+      val (group, pri) =
+        (case worker_task () of
+          SOME task =>
+            (new_group (SOME (Task_Queue.group_of_task task)), Task_Queue.pri_of_task task)
+        | NONE => (new_group NONE, 0));
+      val futures =
+        forks {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} es;
+    in
+      restore_attributes join_results futures
+        handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn)
+    end) ();
+
+
 (* task context for running thread *)
 
 fun task_context name group f x =
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Concurrent/lazy.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -13,12 +13,16 @@
   val lazy_name: string -> (unit -> 'a) -> 'a lazy
   val lazy: (unit -> 'a) -> 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
+  val is_pending: 'a lazy -> bool
   val is_running: 'a lazy -> bool
   val is_finished: 'a lazy -> bool
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
-  val force_list: 'a lazy list -> 'a list
+  val force_value: 'a lazy -> 'a lazy
+  val trim_value: 'a lazy -> 'a lazy
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
+  val map_finished: ('a -> 'b) -> 'a lazy -> 'b lazy
+  val consolidate: 'a lazy list -> 'a lazy list
   val future: Future.params -> 'a lazy -> 'a future
 end;
 
@@ -45,16 +49,18 @@
         Expr _ => NONE
       | Result res => Future.peek res);
 
-fun pending (Value _) = false
-  | pending (Lazy var) =
+
+(* status *)
+
+fun is_value (Value _) = true
+  | is_value (Lazy _) = false;
+
+fun is_pending (Value _) = false
+  | is_pending (Lazy var) =
       (case Synchronized.value var of
         Expr _ => true
       | Result _ => false);
 
-
-
-(* status *)
-
 fun is_running (Value _) = false
   | is_running (Lazy var) =
       (case Synchronized.value var of
@@ -105,12 +111,29 @@
 
 fun force x = Exn.release (force_result x);
 
-fun force_list xs =
-  (List.app (fn x => if pending x then ignore (force_result x) else ()) xs;
-   map force xs);
+fun force_value x = if is_value x then x else value (force x);
+fun trim_value x = if is_pending x then x else force_value x;
+
+
+(* map *)
 
 fun map f x = lazy_name "Lazy.map" (fn () => f (force x));
 
+fun map_finished f x = if is_finished x then value (f (force x)) else map f x;
+
+
+(* consolidate in parallel *)
+
+fun consolidate xs =
+  let
+    val pending =
+      xs |> map_filter (fn x => if is_pending x then SOME (fn () => force_result x) else NONE);
+    val _ =
+      if Multithreading.relevant pending then
+        ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} pending)
+      else List.app (fn e => ignore (e ())) pending;
+  in xs end;
+
 
 (* future evaluation *)
 
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Concurrent/multithreading.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -9,6 +9,7 @@
   val max_threads: unit -> int
   val max_threads_update: int -> unit
   val enabled: unit -> bool
+  val relevant: 'a list -> bool
   val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit
@@ -41,6 +42,8 @@
 fun max_threads_update m = max_threads_state := max_threads_result m;
 fun enabled () = max_threads () > 1;
 
+val relevant = (fn [] => false | [_] => false | _ => enabled ());
+
 end;
 
 
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Concurrent/par_list.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -16,7 +16,6 @@
 
 signature PAR_LIST =
 sig
-  val managed_results: string -> ('a -> 'b) -> 'a list -> 'b Exn.result list
   val map_name: string -> ('a -> 'b) -> 'a list -> 'b list
   val map_independent: ('a -> 'b) -> 'a list -> 'b list
   val map: ('a -> 'b) -> 'a list -> 'b list
@@ -29,27 +28,12 @@
 structure Par_List: PAR_LIST =
 struct
 
-fun managed_results name f xs =
-  if null xs orelse null (tl xs) orelse not (Multithreading.enabled ())
-  then map (Exn.capture f) xs
-  else
-    Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
-      let
-        val (group, pri) =
-          (case Future.worker_task () of
-            SOME task =>
-              (Future.new_group (SOME (Task_Queue.group_of_task task)), Task_Queue.pri_of_task task)
-          | NONE => (Future.new_group NONE, 0));
-        val futures =
-          Future.forks {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
-            (map (fn x => fn () => f x) xs);
-        val results =
-          restore_attributes Future.join_results futures
-            handle exn =>
-              (if Exn.is_interrupt exn then Future.cancel_group group else (); Exn.reraise exn);
-      in results end) ();
+fun forked_results name f xs =
+  if Multithreading.relevant xs
+  then Future.forked_results {name = name, deps = []} (map (fn x => fn () => f x) xs)
+  else map (Exn.capture f) xs;
 
-fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
+fun map_name name f xs = Par_Exn.release_first (forked_results name f xs);
 fun map f = map_name "Par_List.map" f;
 fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all;
 
@@ -57,7 +41,7 @@
   let
     exception FOUND of 'b;
     val results =
-      managed_results "Par_List.get_some"
+      forked_results "Par_List.get_some"
         (fn x => (case f x of NONE => () | SOME y => raise FOUND y)) xs;
   in
     (case get_first (fn Exn.Exn (FOUND res) => SOME res | _ => NONE) results of
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/attrib.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -39,6 +39,7 @@
     (string * thm list) list * Proof.context
   val generic_notes: string -> fact list -> Context.generic ->
     (string * thm list) list * Context.generic
+  val lazy_notes: string -> binding * thm list lazy -> Context.generic -> Context.generic
   val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list
   val attribute_syntax: attribute context_parser -> Token.src -> attribute
   val setup: binding -> attribute context_parser -> string -> theory -> theory
@@ -195,6 +196,9 @@
 fun generic_notes kind facts context = context |>
   Context.mapping_result (global_notes kind facts) (local_notes kind facts);
 
+fun lazy_notes kind arg =
+  Context.mapping (Global_Theory.add_thms_lazy kind arg) (Proof_Context.add_thms_lazy kind arg);
+
 fun eval_thms ctxt srcs = ctxt
   |> Proof_Context.note_thmss ""
     (map_facts_refs
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/class_declaration.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -174,6 +174,8 @@
       | filter_element (Element.Defines _) =
           error ("\"defines\" element not allowed in class specification.")
       | filter_element (Element.Notes _) =
+          error ("\"notes\" element not allowed in class specification.")
+      | filter_element (Element.Lazy_Notes _) =
           error ("\"notes\" element not allowed in class specification.");
     val inferred_elems = map_filter filter_element raw_inferred_elems;
     fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/element.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -20,7 +20,8 @@
     Constrains of (string * 'typ) list |
     Assumes of (Attrib.binding * ('term * 'term list) list) list |
     Defines of (Attrib.binding * ('term * 'term list)) list |
-    Notes of string * (Attrib.binding * ('fact * Token.src list) list) list
+    Notes of string * (Attrib.binding * ('fact * Token.src list) list) list |
+    Lazy_Notes of string * (binding * 'fact lazy)
   type context = (string, string, Facts.ref) ctxt
   type context_i = (typ, term, thm list) ctxt
   val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b,
@@ -51,7 +52,6 @@
   val satisfy_morphism: witness list -> morphism
   val eq_morphism: theory -> thm list -> morphism option
   val init: context_i -> Context.generic -> Context.generic
-  val init': context_i -> Context.generic -> Context.generic
   val activate_i: context_i -> Proof.context -> context_i * Proof.context
   val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
 end;
@@ -82,7 +82,8 @@
   Constrains of (string * 'typ) list |
   Assumes of (Attrib.binding * ('term * 'term list) list) list |
   Defines of (Attrib.binding * ('term * 'term list)) list |
-  Notes of string * (Attrib.binding * ('fact * Token.src list) list) list;
+  Notes of string * (Attrib.binding * ('fact * Token.src list) list) list |
+  Lazy_Notes of string * (binding * 'fact lazy);
 
 type context = (string, string, Facts.ref) ctxt;
 type context_i = (typ, term, thm list) ctxt;
@@ -96,7 +97,8 @@
    | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
       ((binding a, map attrib atts), (term t, map pattern ps))))
    | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
-      ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
+      ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))))
+   | Lazy_Notes (kind, (a, ths)) => Lazy_Notes (kind, (binding a, Lazy.map fact ths));
 
 fun map_ctxt_attrib attrib =
   map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib};
@@ -180,13 +182,17 @@
 
     fun prt_note (a, ths) =
       Pretty.block (Pretty.breaks (flat (prt_binding a " =" :: map prt_fact ths)));
+
+    fun notes_kind "" = "notes"
+      | notes_kind kind = "notes " ^ kind;
   in
     fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes)
      | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)
      | Assumes asms => pretty_items "assumes" "and" (map prt_asm asms)
      | Defines defs => pretty_items "defines" "and" (map prt_def defs)
-     | Notes ("", facts) => pretty_items "notes" "and" (map prt_note facts)
-     | Notes (kind, facts) => pretty_items ("notes " ^ kind) "and" (map prt_note facts)
+     | Notes (kind, facts) => pretty_items (notes_kind kind) "and" (map prt_note facts)
+     | Lazy_Notes (kind, (a, ths)) =>
+        pretty_items (notes_kind kind) "and" [prt_note ((a, []), [(Lazy.force ths, [])])]
   end;
 
 val pretty_ctxt = gen_pretty_ctxt true;
@@ -500,15 +506,8 @@
           |> fold Variable.auto_fixes (map #1 asms)
           |> Proof_Context.add_assms Local_Defs.def_export (map #2 asms);
       in ctxt' end)
-  | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
-
-fun init' elem context =
-  context
-  |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really)
-  |> init elem
-  |> Context.mapping I (fn ctxt =>
-      let val ctxt0 = Context.proof_of context
-      in ctxt |> Context_Position.restore_visible ctxt0 |> Thm.restore_hyps ctxt0 end);
+  | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2
+  | init (Lazy_Notes (kind, ths)) = Attrib.lazy_notes kind ths;
 
 
 (* activate *)
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/expression.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -239,7 +239,8 @@
   | extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts
   | extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms
   | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs
-  | extract_elem (Notes _) = [];
+  | extract_elem (Notes _) = []
+  | extract_elem (Lazy_Notes _) = [];
 
 fun restore_elem (Fixes fixes, css) =
       (fixes ~~ css) |> map (fn ((x, _, mx), cs) =>
@@ -251,7 +252,8 @@
       (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Assumes
   | restore_elem (Defines defs, css) =
       (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines
-  | restore_elem (Notes notes, _) = Notes notes;
+  | restore_elem (elem as Notes _, _) = elem
+  | restore_elem (elem as Lazy_Notes _, _) = elem;
 
 fun prep (_, pats) (ctxt, t :: ts) =
   let val ctxt' = Variable.auto_fixes t ctxt
@@ -298,7 +300,8 @@
       ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd
   | declare_elem _ (Assumes _) ctxt = ctxt
   | declare_elem _ (Defines _) ctxt = ctxt
-  | declare_elem _ (Notes _) ctxt = ctxt;
+  | declare_elem _ (Notes _) ctxt = ctxt
+  | declare_elem _ (Lazy_Notes _) ctxt = ctxt;
 
 
 (** Finish locale elements **)
@@ -346,7 +349,8 @@
   | finish_elem _ _ _ (Constrains _) = Constrains []
   | finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms)
   | finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs)
-  | finish_elem _ _ _ (Notes facts) = Notes facts;
+  | finish_elem _ _ _ (elem as Notes _) = elem
+  | finish_elem _ _ _ (elem as Lazy_Notes _) = elem;
 
 end;
 
@@ -592,7 +596,8 @@
       in (spec', (fold Term.add_frees ts' xs, env, defs)) end
   | eval_text ctxt _ (Defines defs) (spec, binds) =
       (spec, fold (bind_def ctxt o #1 o #2) defs binds)
-  | eval_text _ _ (Notes _) text = text;
+  | eval_text _ _ (Notes _) text = text
+  | eval_text _ _ (Lazy_Notes _) text = text;
 
 fun eval_inst ctxt (loc, morph) text =
   let
@@ -772,9 +777,7 @@
           [(Attrib.internal o K) Locale.witness_add])])) defs)
   | defines_to_notes _ e = e;
 
-fun is_hyp (elem as Assumes asms) = true
-  | is_hyp (elem as Defines defs) = true
-  | is_hyp _ = false;
+val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false;
 
 fun gen_add_locale prep_decl
     binding raw_predicate_binding raw_import raw_body thy =
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/locale.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -59,8 +59,8 @@
   val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
 
   (* Activation *)
+  val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
   val activate_declarations: string * morphism -> Proof.context -> Proof.context
-  val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
   val init: string -> theory -> Proof.context
 
   (* Reasoning about locales *)
@@ -407,6 +407,34 @@
     (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |>
       Pretty.string_of));
 
+fun init_element elem context =
+  context
+  |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really)
+  |> Element.init elem
+  |> Context.mapping I (fn ctxt =>
+      let val ctxt0 = Context.proof_of context
+      in ctxt |> Context_Position.restore_visible ctxt0 |> Thm.restore_hyps ctxt0 end);
+
+
+(* Potentially lazy notes *)
+
+fun lazy_notes thy loc =
+  rev (#notes (the_locale thy loc)) |> maps (fn ((kind, notes), _) =>
+    notes |> map (fn ((b, atts), facts) =>
+      if null atts andalso forall (null o #2) facts andalso false (* FIXME *)
+      then Lazy_Notes (kind, (b, Lazy.value (maps #1 facts)))
+      else Notes (kind, [((b, atts), facts)])));
+
+fun consolidate_notes elems =
+  (elems
+    |> map_filter (fn Lazy_Notes (_, (_, ths)) => SOME ths | _ => NONE)
+    |> Lazy.consolidate;
+   elems);
+
+fun force_notes (Lazy_Notes (kind, (b, ths))) = Notes (kind, [((b, []), [(Lazy.force ths, [])])])
+  | force_notes elem = elem;
+
+
 (* Declarations, facts and entire locale content *)
 
 fun activate_syntax_decls (name, morph) context =
@@ -427,15 +455,11 @@
         NONE => Morphism.identity
       | SOME export => collect_mixins context (name, morph $> export) $> export);
     val morph' = transfer input $> morph $> mixin;
-    val notes' =
-      grouped 100 Par_List.map
-        (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
+    val notes' = grouped 100 Par_List.map (Element.transform_ctxt morph') (lazy_notes thy name);
   in
-    input
-    |> fold_rev
-        (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res) notes'
-      handle ERROR msg => activate_err msg (name, morph) context
-  end;
+    (notes', input) |-> fold (fn elem => fn res =>
+      activ_elem (Element.transform_ctxt (transfer res) elem) res)
+  end handle ERROR msg => activate_err msg (name, morph) context;
 
 fun activate_all name thy activ_elem transfer (marked, input) =
   let
@@ -455,6 +479,16 @@
 
 (** Public activation functions **)
 
+fun activate_facts export dep context =
+  context
+  |> Context_Position.set_visible_generic false
+  |> pair (Idents.get context)
+  |> roundup (Context.theory_of context)
+      (activate_notes init_element Morphism.transfer_morphism'' context export)
+      (the_default Morphism.identity export) dep
+  |-> Idents.put
+  |> Context_Position.restore_visible_generic context;
+
 fun activate_declarations dep = Context.proof_map (fn context =>
   context
   |> Context_Position.set_visible_generic false
@@ -463,16 +497,6 @@
   |-> Idents.put
   |> Context_Position.restore_visible_generic context);
 
-fun activate_facts export dep context =
-  context
-  |> Context_Position.set_visible_generic false
-  |> pair (Idents.get context)
-  |> roundup (Context.theory_of context)
-      (activate_notes Element.init' (Morphism.transfer_morphism o Context.theory_of) context export)
-      (the_default Morphism.identity export) dep
-  |-> Idents.put
-  |> Context_Position.restore_visible_generic context;
-
 fun init name thy =
   let
     val context = Context.Proof (Proof_Context.init_global thy);
@@ -481,7 +505,7 @@
     context
     |> Context_Position.set_visible_generic false
     |> pair empty_idents
-    |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of)
+    |> activate_all name thy init_element Morphism.transfer_morphism''
     |-> (fn marked' => Idents.put (merge_idents (marked, marked')))
     |> Context_Position.restore_visible_generic context
     |> Context.proof_of
@@ -674,10 +698,13 @@
   let
     val locale_ctxt = init name thy;
     fun cons_elem (elem as Notes _) = show_facts ? cons elem
+      | cons_elem (elem as Lazy_Notes _) = show_facts ? cons elem
       | cons_elem elem = cons elem;
     val elems =
       activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, [])
-      |> snd |> rev;
+      |> snd |> rev
+      |> consolidate_notes
+      |> map force_notes;
   in
     Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
       maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/proof_context.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -129,6 +129,7 @@
   val restore_stmt: Proof.context -> Proof.context -> Proof.context
   val add_thms_dynamic: binding * (Context.generic -> thm list) ->
     Proof.context -> string * Proof.context
+  val add_thms_lazy: string -> (binding * thm list lazy) -> Proof.context -> Proof.context
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
@@ -1062,27 +1063,36 @@
 
 local
 
-fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
-  | update_thms flags (b, SOME ths) ctxt = ctxt |> map_facts
-      (Facts.add_static (Context.Proof ctxt) flags (b, ths) #> snd);
+fun add_facts {index} arg ctxt = ctxt
+  |> map_facts_result (Facts.add_static (Context.Proof ctxt) {strict = false, index = index} arg);
+
+fun update_facts flags (b, SOME ths) ctxt = ctxt |> add_facts flags (b, Lazy.value ths) |> #2
+  | update_facts _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b));
 
 in
 
-fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt =>
+fun add_thms_lazy kind (b, ths) ctxt =
   let
     val name = full_name ctxt b;
-    val facts = Global_Theory.name_thmss false name raw_facts;
+    val ths' = Lazy.map (Global_Theory.name_thms true false name #> map (Thm.kind_rule kind)) ths;
+    val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
+  in ctxt' end;
+
+fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn ctxt =>
+  let
+    val name = full_name ctxt b;
+    val facts' = Global_Theory.name_thmss false name facts;
     fun app (ths, atts) =
       fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
-    val (res, ctxt') = fold_map app facts ctxt;
+    val (res, ctxt') = fold_map app facts' ctxt;
     val thms = Global_Theory.name_thms false false name (flat res);
-    val index = is_stmt ctxt;
-  in ((name, thms), ctxt' |> update_thms {strict = false, index = index} (b, SOME thms)) end);
+    val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms);
+  in ((name, thms), ctxt'') end);
 
 fun put_thms index thms ctxt = ctxt
   |> map_naming (K Name_Space.local_naming)
   |> Context_Position.set_visible false
-  |> update_thms {strict = false, index = index} (apfst Binding.name thms)
+  |> update_facts {index = index} (apfst Binding.name thms)
   |> Context_Position.restore_visible ctxt
   |> restore_naming ctxt;
 
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/PIDE/execution.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -162,13 +162,12 @@
 fun fork_prints exec_id =
   (case Inttab.lookup (#2 (get_state ())) exec_id of
     SOME (_, prints) =>
-      if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
-      then List.app (fn {body, ...} => body ()) (rev prints)
-      else
+      if Multithreading.relevant prints then
         let val pos = Position.thread_data () in
           List.app (fn {name, pri, body} =>
             ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
         end
+      else List.app (fn {body, ...} => body ()) (rev prints)
   | NONE => raise Fail (unregistered exec_id));
 
 
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/facts.ML
--- a/src/Pure/facts.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/facts.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -40,7 +40,7 @@
   val could_unify: T -> term -> (thm * Position.T) list
   val merge: T * T -> T
   val add_static: Context.generic -> {strict: bool, index: bool} ->
-    binding * thm list -> T -> string * T
+    binding * thm list lazy -> T -> string * T
   val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
   val del: string -> T -> T
   val hide: bool -> string -> T -> T
@@ -130,7 +130,7 @@
 
 (* datatypes *)
 
-datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
+datatype fact = Static of thm list lazy | Dynamic of Context.generic -> thm list;
 
 datatype T = Facts of
  {facts: fact Name_Space.table,
@@ -178,7 +178,7 @@
 fun lookup context facts name =
   (case Name_Space.lookup (facts_of facts) name of
     NONE => NONE
-  | SOME (Static ths) => SOME {dynamic = false, thms = ths}
+  | SOME (Static ths) => SOME {dynamic = false, thms = Lazy.force ths}
   | SOME (Dynamic f) => SOME {dynamic = true, thms = f context});
 
 fun retrieve context facts (xname, pos) =
@@ -203,23 +203,34 @@
 
 local
 
+fun fold_static_lazy f =
+  Name_Space.fold_table (fn (a, Static ths) => f (a, ths) | _ => I) o facts_of;
+
+fun consolidate facts =
+  let
+    val pending =
+      (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_pending ths then cons ths else I);
+    val _ = Lazy.consolidate pending;
+  in facts end;
+
 fun included verbose prev_facts facts name =
   not (exists (fn prev => defined prev name) prev_facts orelse
     not verbose andalso is_concealed facts name);
 
 in
 
-fun fold_static f =
-  Name_Space.fold_table (fn (a, Static ths) => f (a, ths) | _ => I) o facts_of;
+fun fold_static f facts =
+  fold_static_lazy (f o apsnd Lazy.force) (consolidate facts);
 
 fun dest_static verbose prev_facts facts =
   fold_static (fn (a, ths) => included verbose prev_facts facts a ? cons (a, ths)) facts []
   |> sort_by #1;
 
 fun dest_all context verbose prev_facts facts =
-  Name_Space.fold_table (fn (a, fact) =>
-    let val ths = (case fact of Static ths => ths | Dynamic f => f context)
-    in included verbose prev_facts facts a ? cons (a, ths) end) (facts_of facts) []
+  (facts_of (consolidate facts), [])
+  |-> Name_Space.fold_table (fn (a, fact) =>
+    let val ths = (case fact of Static ths => Lazy.force ths | Dynamic f => f context)
+    in included verbose prev_facts facts a ? cons (a, ths) end)
   |> sort_by #1;
 
 end;
@@ -245,24 +256,23 @@
   in make_facts facts' props' end;
 
 
-(* add static entries *)
+(* add entries *)
+
+fun add_prop pos th =
+  Net.insert_term (K false) (Thm.full_prop_of th, (th, pos));
 
 fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
   let
-    val ths' = map Thm.trim_context ths;
-    val pos = Binding.pos_of (Binding.default_pos b);
-
+    val ths' = ths
+      |> index ? Lazy.force_value
+      |> Lazy.map_finished (map Thm.trim_context);
     val (name, facts') =
       if Binding.is_empty b then ("", facts)
       else Name_Space.define context strict (b, Static ths') facts;
-
     val props' = props
-      |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, (th, pos))) ths';
+      |> index ? fold (add_prop (Binding.pos_of (Binding.default_pos b))) (Lazy.force ths');
   in (name, make_facts facts' props') end;
 
-
-(* add dynamic entries *)
-
 fun add_dynamic context (b, f) (Facts {facts, props}) =
   let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
   in (name, make_facts facts' props) end;
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/global_theory.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -24,6 +24,7 @@
   val name_thm: bool -> bool -> string -> thm -> thm
   val name_thms: bool -> bool -> string -> thm list -> thm list
   val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
+  val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
   val store_thms: binding * thm list -> theory -> thm list * theory
   val store_thm: binding * thm -> theory -> thm * theory
   val store_thm_open: binding * thm -> theory -> thm * theory
@@ -124,19 +125,28 @@
 
 (* enter_thms *)
 
-fun register_proofs thms thy = (thms, Thm.register_proofs thms thy);
+fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
 
-fun enter_thms pre_name post_name app_att (b, thms) thy =
-  if Binding.is_empty b
-  then app_att thms thy |-> register_proofs
+fun add_facts arg thy =
+  thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2);
+
+fun add_thms_lazy kind (b, thms) thy =
+  if Binding.is_empty b then Thm.register_proofs thms thy
   else
     let
       val name = Sign.full_name thy b;
-      val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
-      val thms'' = map (Thm.transfer thy') thms';
-      val thy'' = thy' |> Data.map
-        (Facts.add_static (Context.Theory thy') {strict = true, index = false} (b, thms'') #> snd);
-    in (thms'', thy'') end;
+      val thms' = Lazy.map_finished (name_thms true true name #> map (Thm.kind_rule kind)) thms;
+    in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end;
+
+fun enter_thms pre_name post_name app_att (b, thms) thy =
+  if Binding.is_empty b then app_att thms thy |-> register_proofs
+  else
+    let
+      val name = Sign.full_name thy b;
+      val (thms', thy') =
+        app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
+      val thy'' = thy' |> add_facts (b, Lazy.value thms');
+    in (map (Thm.transfer thy'') thms', thy'') end;
 
 
 (* store_thm(s) *)
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/more_thm.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -112,7 +112,7 @@
   val tag: string * string -> attribute
   val untag: string -> attribute
   val kind: string -> attribute
-  val register_proofs: thm list -> theory -> theory
+  val register_proofs: thm list lazy -> theory -> theory
   val consolidate_theory: theory -> unit
   val show_consts_raw: Config.raw
   val show_consts: bool Config.T
@@ -643,17 +643,21 @@
 
 structure Proofs = Theory_Data
 (
-  type T = thm list;
+  type T = thm list lazy list;
   val empty = [];
   fun extend _ = empty;
   fun merge _ = empty;
 );
 
-fun register_proofs more_thms =
-  Proofs.map (fold (cons o Thm.trim_context) more_thms);
+fun register_proofs ths =
+  (Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths);
 
 fun consolidate_theory thy =
-  Thm.consolidate (map (Thm.transfer thy) (rev (Proofs.get thy)));
+  let
+    val proofs = Proofs.get thy;
+    val pending = fold (fn ths => if Lazy.is_pending ths then cons ths else I) [] proofs;
+    val _ = Lazy.consolidate pending;
+  in Thm.consolidate (maps (map (Thm.transfer thy) o Lazy.force) (rev proofs)) end;
 
 
 
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/morphism.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -39,6 +39,8 @@
   val fact_morphism: string -> (thm list -> thm list) -> morphism
   val thm_morphism: string -> (thm -> thm) -> morphism
   val transfer_morphism: theory -> morphism
+  val transfer_morphism': Proof.context -> morphism
+  val transfer_morphism'': Context.generic -> morphism
   val trim_context_morphism: morphism
   val instantiate_morphism:
     ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism
@@ -120,6 +122,9 @@
 fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]};
 
 val transfer_morphism = thm_morphism "transfer" o Thm.transfer;
+val transfer_morphism' = transfer_morphism o Proof_Context.theory_of;
+val transfer_morphism'' = transfer_morphism o Context.theory_of;
+
 val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
 
 fun instantiate_morphism ([], []) = identity
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/par_tactical.ML
--- a/src/Pure/par_tactical.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/par_tactical.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -41,20 +41,22 @@
 in
 
 fun PARALLEL_GOALS tac st =
-  if not (Multithreading.enabled ()) orelse Thm.nprems_of st <= 1 then DETERM tac st
-  else
-    let val subgoals = map (Thm.adjust_maxidx_cterm ~1) (Drule.strip_imp_prems (Thm.cprop_of st)) in
-      if exists (fn sg => Thm.maxidx_of_cterm sg >= 0) subgoals then DETERM tac st
-      else
-        let
-          fun try_tac g =
-            (case SINGLE tac g of
-              NONE => raise FAILED ()
-            | SOME g' => g');
-          val results = Par_List.map (try_tac o Goal.init) subgoals;
-        in EVERY (map retrofit (rev results)) st end
-        handle FAILED () => Seq.empty
-    end;
+  let
+    val goals =
+      Drule.strip_imp_prems (Thm.cprop_of st)
+      |> map (Thm.adjust_maxidx_cterm ~1);
+  in
+    if Multithreading.relevant goals andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals then
+      let
+        fun try_goal g =
+          (case SINGLE tac (Goal.init g) of
+            NONE => raise FAILED ()
+          | SOME st' => st');
+        val results = Par_List.map try_goal goals;
+      in EVERY (map retrofit (rev results)) st
+      end handle FAILED () => Seq.empty
+    else DETERM tac st
+  end;
 
 end;
 
diff -r 67909bfc3923 -r 738f170f43ee src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/proofterm.ML	Tue Feb 20 09:34:03 2018 +0000
@@ -199,7 +199,7 @@
 
 val consolidate =
   maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
-  #> Lazy.force_list #> ignore;
+  #> Lazy.consolidate #> map Lazy.force #> ignore;
 
 fun make_thm_node name prop body =
   Thm_Node {name = name, prop = prop, body = body,