author | haftmann |
Fri, 21 Aug 2020 18:59:29 +0000 | |
changeset 72186 | bdf77466b6c8 |
parent 72185 | 0f9ebade33ab |
child 72187 | e4aecb0c7296 |
--- a/src/HOL/Statespace/state_space.ML Fri Aug 21 12:43:07 2020 +0100 +++ b/src/HOL/Statespace/state_space.ML Fri Aug 21 18:59:29 2020 +0000 @@ -299,7 +299,7 @@ fun add_declaration name decl thy = thy |> Named_Target.init name - |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy) + |> (fn lthy => Local_Theory.declaration {syntax = true, pervasive = false} (decl lthy) lthy) |> Local_Theory.exit_global; fun parent_components thy (Ts, pname, renaming) =