prevent subscription in nested contexts explicitly -- at foundational and user level

--- a/src/Pure/Isar/expression.ML	Thu May 01 09:30:33 2014 +0200
+++ b/src/Pure/Isar/expression.ML	Thu May 01 09:30:34 2014 +0200
@@ -958,8 +958,10 @@
 fun interpret x = gen_interpret cert_interpretation x;
 fun interpret_cmd x = gen_interpret read_interpretation x;
 
-fun permanent_interpretation x =
-  gen_local_theory_interpretation cert_interpretation (K Local_Theory.subscription) x;
+fun permanent_interpretation expression raw_eqns =
+  Local_Theory.assert_bottom true
+  #> gen_local_theory_interpretation cert_interpretation
+    (K Local_Theory.subscription) expression raw_eqns;
 
 fun ephemeral_interpretation x =
   gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x;

--- a/src/Pure/Isar/local_theory.ML	Thu May 01 09:30:33 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu May 01 09:30:34 2014 +0200
@@ -256,7 +256,6 @@
 
 fun operation f lthy = f (operations_of lthy) lthy;
 fun operation2 f x y = operation (fn ops => f ops x y);
-fun operation3 f x y z = operation (fn ops => f ops x y z);
 
 val pretty = operation #pretty;
 val abbrev = operation2 #abbrev;
@@ -264,7 +263,8 @@
 val define_internal = operation2 #define true;
 val notes_kind = operation2 #notes;
 val declaration = operation2 #declaration;
-val subscription = operation3 #subscription;
+fun subscription dep_morph mixin export =
+  assert_bottom true #> operation (fn ops => #subscription ops dep_morph mixin export);
 
 
 (* basic derived operations *)

--- a/src/Tools/permanent_interpretation.ML	Thu May 01 09:30:33 2014 +0200
+++ b/src/Tools/permanent_interpretation.ML	Thu May 01 09:30:34 2014 +0200
@@ -85,9 +85,10 @@
 
 (* interpretation with permanent registration *)
 
-fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy =
-  generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.subscription
-    expression raw_defs raw_eqns lthy
+fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
+  Local_Theory.assert_bottom true
+  #> generic_interpretation prep_interpretation Element.witness_proof_eqs
+    Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
 
 in