src/Pure/Isar/expression.ML
changeset 56809 b60009672a65
parent 56723 a8f71445c265
child 57181 2d13bf9ea77b
     1.1 --- a/src/Pure/Isar/expression.ML	Thu May 01 09:30:33 2014 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu May 01 09:30:34 2014 +0200
     1.3 @@ -958,8 +958,10 @@
     1.4  fun interpret x = gen_interpret cert_interpretation x;
     1.5  fun interpret_cmd x = gen_interpret read_interpretation x;
     1.6  
     1.7 -fun permanent_interpretation x =
     1.8 -  gen_local_theory_interpretation cert_interpretation (K Local_Theory.subscription) x;
     1.9 +fun permanent_interpretation expression raw_eqns =
    1.10 +  Local_Theory.assert_bottom true
    1.11 +  #> gen_local_theory_interpretation cert_interpretation
    1.12 +    (K Local_Theory.subscription) expression raw_eqns;
    1.13  
    1.14  fun ephemeral_interpretation x =
    1.15    gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x;