| changeset 66334 | b210ae666a42 |
| parent 63402 | f199837304d7 |
| child 67450 | b0ae74b86ef3 |
--- a/src/HOL/Statespace/state_space.ML Fri Aug 04 08:12:37 2017 +0200 +++ b/src/HOL/Statespace/state_space.ML Fri Aug 04 08:12:37 2017 +0200 @@ -298,7 +298,7 @@ fun add_declaration name decl thy = thy - |> Named_Target.init NONE name + |> Named_Target.init name |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy) |> Local_Theory.exit_global;