changeset 35682 | 5e6811f4294b |
parent 35626 | 06197484c6ad |
child 35741 | 4f3660a3e5af |
--- a/src/HOL/Tools/typedef.ML Tue Mar 09 23:32:13 2010 +0100 +++ b/src/HOL/Tools/typedef.ML Tue Mar 09 23:32:49 2010 +0100 @@ -130,7 +130,7 @@ in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end; fun typedef_result inhabited = - Typedecl.typedecl (tname, vs, mx) + Typedecl.typedecl_global (tname, vs, mx) #> snd #> Sign.add_consts_i [(Rep_name, newT --> oldT, NoSyn),