equal
deleted
inserted
replaced
79 |
79 |
80 fun interpretation f = |
80 fun interpretation f = |
81 Typedef_Plugin.interpretation typedef_plugin |
81 Typedef_Plugin.interpretation typedef_plugin |
82 (fn name => fn lthy => |
82 (fn name => fn lthy => |
83 lthy |
83 lthy |
84 |> Local_Theory.map_naming |
84 |> Local_Theory.map_background_naming |
85 (Name_Space.root_path #> Name_Space.add_path (Long_Name.qualifier name)) |
85 (Name_Space.root_path #> Name_Space.add_path (Long_Name.qualifier name)) |
86 |> f name |
86 |> f name |
87 |> Local_Theory.restore_naming lthy); |
87 |> Local_Theory.restore_background_naming lthy); |
88 |
88 |
89 |
89 |
90 (* primitive typedef axiomatization -- for fresh typedecl *) |
90 (* primitive typedef axiomatization -- for fresh typedecl *) |
91 |
91 |
92 fun mk_inhabited A = |
92 fun mk_inhabited A = |