changeset 35626 | 06197484c6ad |
parent 35625 | 9c818cab0dd0 |
child 35682 | 5e6811f4294b |
--- a/src/HOL/Tools/typedef.ML Sun Mar 07 12:19:47 2010 +0100 +++ b/src/HOL/Tools/typedef.ML Sun Mar 07 12:47:02 2010 +0100 @@ -130,7 +130,7 @@ in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end; fun typedef_result inhabited = - Object_Logic.typedecl (tname, vs, mx) + Typedecl.typedecl (tname, vs, mx) #> snd #> Sign.add_consts_i [(Rep_name, newT --> oldT, NoSyn),