equal
deleted
inserted
replaced
193 identifier = identifier}; |
193 identifier = identifier}; |
194 in |
194 in |
195 lthy |> Local_Theory.declaration false (fn phi => fn context => |
195 lthy |> Local_Theory.declaration false (fn phi => fn context => |
196 let |
196 let |
197 val b' = Morphism.binding phi b; |
197 val b' = Morphism.binding phi b; |
198 val simproc' = morph_simproc phi simproc; |
198 val simproc' = transform_simproc phi simproc; |
199 in |
199 in |
200 context |
200 context |
201 |> Data.map (fn (ss, tab) => |
201 |> Data.map (fn (ss, tab) => |
202 (ss addsimprocs [simproc'], |
202 (ss addsimprocs [simproc'], |
203 #2 (Name_Space.define (Context.proof_of context) true naming (b', simproc') tab))) |
203 #2 (Name_Space.define (Context.proof_of context) true naming (b', simproc') tab))) |
296 |
296 |
297 val add_del = |
297 val add_del = |
298 (Args.del -- Args.colon >> K (op delsimprocs) || |
298 (Args.del -- Args.colon >> K (op delsimprocs) || |
299 Scan.option (Args.add -- Args.colon) >> K (op addsimprocs)) |
299 Scan.option (Args.add -- Args.colon) >> K (op addsimprocs)) |
300 >> (fn f => fn simproc => fn phi => Thm.declaration_attribute |
300 >> (fn f => fn simproc => fn phi => Thm.declaration_attribute |
301 (K (map_ss (fn ss => f (ss, [morph_simproc phi simproc]))))); |
301 (K (map_ss (fn ss => f (ss, [transform_simproc phi simproc]))))); |
302 |
302 |
303 in |
303 in |
304 |
304 |
305 val simproc_att = |
305 val simproc_att = |
306 (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) => |
306 (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) => |