# HG changeset patch
# User paulson
# Date 1524604945 -3600
# Node ID 412fe0623c5d1619ef44ccbb17d293ea2a8ba58f
# Parent  0a6d6ba383dc1d1a3520437b0bd5411dd89317bc# Parent  eda52f4cd4e44b594dcdbc8aad165ba4204cd1f2
merged

diff -r eda52f4cd4e4 -r 412fe0623c5d src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Apr 24 22:22:08 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Apr 24 22:22:25 2018 +0100
@@ -420,7 +420,6 @@
 
 fun make_notes kind = map (fn ((b, atts), facts) =>
   if null atts andalso forall (null o #2) facts
-    andalso not (Proofterm.proofs_enabled ()) (* FIXME *)
   then Lazy_Notes (kind, (b, Lazy.value (maps #1 facts)))
   else Notes (kind, [((b, atts), facts)]));
 
diff -r eda52f4cd4e4 -r 412fe0623c5d src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Apr 24 22:22:08 2018 +0100
+++ b/src/Pure/proofterm.ML	Tue Apr 24 22:22:25 2018 +0100
@@ -1610,16 +1610,14 @@
     val argsP = map OfClass outer_constraints @ map Hyp hyps;
 
     fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
-    fun make_body () =
-      make_body0 (shrink_proof (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
     val body0 =
       if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
-      else if not (Multithreading.parallel_proofs_enabled 1) then Future.value (make_body ())
       else
         (singleton o Future.cond_forks)
           {name = "Proofterm.prepare_thm_proof", group = NONE,
-            deps = [], pri = 0, interrupts = true}
-          make_body;
+            deps = [], pri = 1, interrupts = true}
+          (fn () =>
+            make_body0 (shrink_proof (rew_proof thy (fold_rev implies_intr_proof hyps prf))));
 
     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
     val (i, body') =