# HG changeset patch
# User wenzelm
# Date 1519391568 -3600
# Node ID 2d9918f5b33cb45c15ad842310efe96053de1d37
# Parent  454dfdaf021deea7f69b89dba9538dd5992a86aa
command 'interpret' no longer exposes resulting theorems as literal facts;

diff -r 454dfdaf021d -r 2d9918f5b33c NEWS
--- a/NEWS	Fri Feb 23 13:09:45 2018 +0100
+++ b/NEWS	Fri Feb 23 14:12:48 2018 +0100
@@ -167,6 +167,15 @@
 latex and bibtex process. Minor INCOMPATIBILITY.
 
 
+*** Isar ***
+
+* Command 'interpret' no longer exposes resulting theorems as literal
+facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This
+improves modularity of proofs and scalability of locale interpretation.
+Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
+(e.g. use 'find_theorems' or 'try' to figure this out).
+
+
 *** HOL ***
 
 * Clarifed theorem names:
diff -r 454dfdaf021d -r 2d9918f5b33c src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Fri Feb 23 13:09:45 2018 +0100
+++ b/src/Pure/Isar/interpretation.ML	Fri Feb 23 14:12:48 2018 +0100
@@ -175,10 +175,14 @@
     fun setup_proof after_qed propss eqns goal_ctxt =
       Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
         propss eqns goal_ctxt state;
+    fun add_registration reg mixin export ctxt = ctxt
+      |> Proof_Context.set_stmt false
+      |> Context.proof_map (Locale.add_registration reg mixin export)
+      |> Proof_Context.restore_stmt ctxt;
   in
     Proof.context_of state
     |> generic_interpretation prep_interpretation setup_proof
-      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression [] raw_eqns
+      Attrib.local_notes add_registration expression [] raw_eqns
   end;
 
 in