| changeset 19630 | d370c3f5d3b2 |
| parent 19517 | 73361110b570 |
| child 19661 | baab85f25e0e |
--- a/src/Pure/Isar/local_theory.ML Sat May 13 02:51:40 2006 +0200 +++ b/src/Pure/Isar/local_theory.ML Sat May 13 02:51:42 2006 +0200 @@ -248,7 +248,7 @@ local fun add_def (name, prop) = - Theory.add_defs_i false [(name, prop)] #> (fn thy => + Theory.add_defs_i false false [(name, prop)] #> (fn thy => let val th = Thm.get_axiom_i thy (Sign.full_name thy name); val cert = Thm.cterm_of thy;