equal
deleted
inserted
replaced
192 identifier = identifier} |
192 identifier = identifier} |
193 |> morph_simproc (LocalTheory.target_morphism lthy); |
193 |> morph_simproc (LocalTheory.target_morphism lthy); |
194 in |
194 in |
195 lthy |> LocalTheory.declaration (fn phi => |
195 lthy |> LocalTheory.declaration (fn phi => |
196 let |
196 let |
197 val b' = Morphism.name phi (Name.binding name); |
197 val b' = Morphism.binding phi (Binding.name name); |
198 val simproc' = morph_simproc phi simproc; |
198 val simproc' = morph_simproc phi simproc; |
199 in |
199 in |
200 Simprocs.map (fn simprocs => |
200 Simprocs.map (fn simprocs => |
201 NameSpace.table_declare naming (b', simproc') simprocs |> snd |
201 NameSpace.bind naming (b', simproc') simprocs |> snd |
202 handle Symtab.DUP dup => err_dup_simproc dup) |
202 handle Symtab.DUP dup => err_dup_simproc dup) |
203 #> map_ss (fn ss => ss addsimprocs [simproc']) |
203 #> map_ss (fn ss => ss addsimprocs [simproc']) |
204 end) |
204 end) |
205 end; |
205 end; |
206 |
206 |