# HG changeset patch
# User wenzelm
# Date 1532049284 -7200
# Node ID 5820f0f379ae8ae4530f5fe51c16def67782d019
# Parent  4ce18f389f53b89d699fc8d5a478c19821bb96ab
added system option "strict_facts";

diff -r 4ce18f389f53 -r 5820f0f379ae NEWS
--- a/NEWS	Wed Jul 18 20:51:23 2018 +0200
+++ b/NEWS	Fri Jul 20 03:14:44 2018 +0200
@@ -22,6 +22,12 @@
 * Global facts need to be closed: no free variables and no hypotheses.
 Rare INCOMPATIBILITY.
 
+* Facts stemming from locale interpretation are subject to lazy
+evaluation for improved performance. Rare INCOMPATIBILITY: errors
+stemming from interpretation morphisms might be deferred and thus
+difficult to locate; enable system option "strict_facts" temporarily to
+avoid this.
+
 * Marginal comments need to be written exclusively in the new-style form
 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
 supported. INCOMPATIBILITY, use the command-line tool "isabelle
diff -r 4ce18f389f53 -r 5820f0f379ae etc/options
--- a/etc/options	Wed Jul 18 20:51:23 2018 +0200
+++ b/etc/options	Fri Jul 20 03:14:44 2018 +0200
@@ -92,6 +92,8 @@
   -- "if true then some tools will OMIT some proofs"
 option skip_proofs : bool = false
   -- "skip over proofs (implicit 'sorry')"
+option strict_facts : bool = false
+  -- "force lazy facts when defined in context"
 
 
 section "Global Session Parameters"
diff -r 4ce18f389f53 -r 5820f0f379ae src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jul 18 20:51:23 2018 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Jul 20 03:14:44 2018 +0200
@@ -1077,7 +1077,8 @@
 fun add_thms_lazy kind (b, ths) ctxt =
   let
     val name = full_name ctxt b;
-    val ths' = ths
+    val ths' =
+      Global_Theory.check_thms_lazy ths
       |> Lazy.map_finished (Global_Theory.name_thms true false name #> map (Thm.kind_rule kind));
     val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
   in ctxt' end;
diff -r 4ce18f389f53 -r 5820f0f379ae src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Wed Jul 18 20:51:23 2018 +0200
+++ b/src/Pure/global_theory.ML	Fri Jul 20 03:14:44 2018 +0200
@@ -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 check_thms_lazy: thm list lazy -> thm list lazy
   val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
   val store_thm: binding * thm -> theory -> thm * theory
   val store_thm_open: binding * thm -> theory -> thm * theory
@@ -156,12 +157,16 @@
     thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
   end;
 
+fun check_thms_lazy (thms: thm list lazy) =
+  if Options.default_bool "strict_facts" then (Lazy.force thms; thms) else thms;
+
 fun add_thms_lazy kind (b, thms) thy =
-  if Binding.is_empty b then Thm.register_proofs thms thy
+  if Binding.is_empty b then Thm.register_proofs (check_thms_lazy thms) thy
   else
     let
       val name = Sign.full_name thy b;
-      val thms' = thms
+      val thms' =
+        check_thms_lazy thms
         |> Lazy.map_finished (name_thms true true name #> map (Thm.kind_rule kind));
     in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end;