1.1 --- a/thys/Simpl/hoare_package.ML Fri Nov 06 15:02:13 2009 +0100
1.2 +++ b/thys/Simpl/hoare_package.ML Sat Nov 07 18:09:07 2009 +0100
1.3 @@ -739,7 +739,7 @@
1.4 fun add_declaration name decl thy =
1.5 thy
1.6 |> TheoryTarget.init name
1.7 - |> LocalTheory.declaration decl
1.8 + |> LocalTheory.declaration false decl
1.9 |> LocalTheory.exit
1.10 |> ProofContext.theory_of;
1.11
1.12 @@ -1273,7 +1273,7 @@
1.13 ctxt
1.14 |> ProofContext.theory_of
1.15 |> TheoryTarget.init (SOME lname)
1.16 - |> LocalTheory.declaration parameter_info_decl
1.17 + |> LocalTheory.declaration false parameter_info_decl
1.18 |> (fn lthy => if has_body name
1.19 then snd (LocalTheory.define Thm.definitionK (def lthy) lthy)
1.20 else lthy)