| changeset 38388 | 94d5624dd1f7 |
| parent 38350 | 480b2de9927c |
| child 38757 | 2b3e054ae6fc |
--- a/src/HOL/Tools/typedef.ML Thu Aug 12 09:00:19 2010 +0200 +++ b/src/HOL/Tools/typedef.ML Thu Aug 12 13:23:46 2010 +0200 @@ -268,7 +268,7 @@ in typedef_result inhabited lthy' end; fun add_typedef_global def opt_name typ set opt_morphs tac = - Named_Target.init NONE + Named_Target.theory_init #> add_typedef def opt_name typ set opt_morphs tac #> Local_Theory.exit_result_global (apsnd o transform_info);