src/Pure/Isar/expression.ML
changeset 52118 2a976115c7c3
parent 51750 cb154917a496
child 52119 90ba620333d0
     1.1 --- a/src/Pure/Isar/expression.ML	Wed May 22 19:44:51 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed May 22 22:56:17 2013 +0200
     1.3 @@ -879,8 +879,10 @@
     1.4      val is_theory = Option.map #target (Named_Target.peek lthy) = SOME ""
     1.5        andalso Local_Theory.level lthy = 1;
     1.6      val activate = if is_theory then add_registration else activate_local_theory;
     1.7 +    val mark_brittle = if is_theory then I else Local_Theory.mark_brittle;
     1.8    in
     1.9      lthy
    1.10 +    |> mark_brittle
    1.11      |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    1.12          Local_Theory.notes_kind activate expression raw_eqns
    1.13    end;