# HG changeset patch
# User haftmann
# Date 1548054507 0
# Node ID 1c201e4792cb6dd749ecb93474a51874131c21a8
# Parent  920fe0a2fd2284f4a711c307b6ebdbd0156a8788
Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space

diff -r 920fe0a2fd22 -r 1c201e4792cb NEWS
--- a/NEWS	Mon Jan 21 22:46:25 2019 +0100
+++ b/NEWS	Mon Jan 21 07:08:27 2019 +0000
@@ -134,6 +134,11 @@
 
 *** ML ***
 
+* Local_Theory.reset is no longer available in user space. Regular
+definitional packages should use balanced blocks of
+Local_Theory.open_target versus Local_Theory.close_target instead,
+or the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
+
 * Original PolyML.pointerEq is retained as a convenience for tools that
 don't use Isabelle/ML (where this is called "pointer_eq").
 
diff -r 920fe0a2fd22 -r 1c201e4792cb src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Jan 21 22:46:25 2019 +0100
+++ b/src/Pure/Isar/local_theory.ML	Mon Jan 21 07:08:27 2019 +0000
@@ -23,7 +23,6 @@
 sig
   type operations
   val assert: local_theory -> local_theory
-  val reset: local_theory -> local_theory
   val level: Proof.context -> int
   val assert_bottom: local_theory -> local_theory
   val mark_brittle: local_theory -> local_theory
@@ -83,7 +82,13 @@
     local_theory -> 'b * local_theory
 end;
 
-structure Local_Theory: LOCAL_THEORY =
+signature PRIVATE_LOCAL_THEORY =
+sig
+  include LOCAL_THEORY
+  val reset: local_theory -> local_theory
+end
+
+structure Local_Theory: PRIVATE_LOCAL_THEORY =
 struct
 
 (** local theory data **)
diff -r 920fe0a2fd22 -r 1c201e4792cb src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jan 21 22:46:25 2019 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Jan 21 07:08:27 2019 +0000
@@ -749,3 +749,5 @@
 end;
 
 end;
+
+structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end;