changeset 33457 | 0fc03a81c27c |
parent 33222 | 89ced80833ac |
child 33519 | e31a85f92ce9 |
--- a/src/HOL/Statespace/state_space.ML Thu Nov 05 22:06:46 2009 +0100 +++ b/src/HOL/Statespace/state_space.ML Thu Nov 05 22:08:47 2009 +0100 @@ -355,7 +355,7 @@ fun add_declaration name decl thy = thy |> TheoryTarget.init name - |> (fn lthy => LocalTheory.declaration (decl lthy) lthy) + |> (fn lthy => LocalTheory.declaration false (decl lthy) lthy) |> LocalTheory.exit_global; fun parent_components thy (Ts, pname, renaming) =