equal
deleted
inserted
replaced
140 || Scan.succeed no_map_rel; |
140 || Scan.succeed no_map_rel; |
141 |
141 |
142 fun typedef (b, Ts, mx) set opt_morphs tac lthy = |
142 fun typedef (b, Ts, mx) set opt_morphs tac lthy = |
143 let |
143 let |
144 (*Work around loss of qualification in "typedef" axioms by replicating it in the name*) |
144 (*Work around loss of qualification in "typedef" axioms by replicating it in the name*) |
145 val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b; |
145 val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b; |
146 val ((name, info), (lthy, lthy_old)) = |
146 val ((name, info), (lthy, lthy_old)) = |
147 lthy |
147 lthy |
148 |> Local_Theory.conceal |
148 |> Local_Theory.conceal |
149 |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac |
149 |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac |
150 ||> Local_Theory.restore_naming lthy |
150 ||> Local_Theory.restore_naming lthy |