# HG changeset patch # User haftmann # Date 1398929434 -7200 # Node ID b60009672a65e8445b0b2f5b8f0acb5ff4dbed89 # Parent d4a790cb47e8f7c2f7fbec4ee5dad68c89834c8c prevent subscription in nested contexts explicitly -- at foundational and user level diff -r d4a790cb47e8 -r b60009672a65 src/Pure/Isar/expression.ML --- 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; diff -r d4a790cb47e8 -r b60009672a65 src/Pure/Isar/local_theory.ML --- 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 *) diff -r d4a790cb47e8 -r b60009672a65 src/Tools/permanent_interpretation.ML --- 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