187 |
187 |
188 local |
188 local |
189 |
189 |
190 fun gen_simproc prep {name = b, lhss, proc, identifier} lthy = |
190 fun gen_simproc prep {name = b, lhss, proc, identifier} lthy = |
191 let |
191 let |
192 val naming = Local_Theory.naming_of lthy; |
|
193 val simproc = make_simproc |
192 val simproc = make_simproc |
194 {name = Name_Space.full_name naming b, |
193 {name = Local_Theory.full_name lthy b, |
195 lhss = |
194 lhss = |
196 let |
195 let |
197 val lhss' = prep lthy lhss; |
196 val lhss' = prep lthy lhss; |
198 val ctxt' = fold Variable.auto_fixes lhss' lthy; |
197 val ctxt' = fold Variable.auto_fixes lhss' lthy; |
199 in Variable.export_terms ctxt' lthy lhss' end |
198 in Variable.export_terms ctxt' lthy lhss' end |
200 |> map (Thm.cterm_of (Proof_Context.theory_of lthy)), |
199 |> map (Thm.cterm_of (Proof_Context.theory_of lthy)), |
201 proc = proc, |
200 proc = proc, |
202 identifier = identifier}; |
201 identifier = identifier}; |
203 in |
202 in |
204 lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context => |
203 lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => |
205 let |
204 let |
|
205 val naming = Proof_Context.target_naming_of context; |
206 val b' = Morphism.binding phi b; |
206 val b' = Morphism.binding phi b; |
207 val simproc' = transform_simproc phi simproc; |
207 val simproc' = transform_simproc phi simproc; |
208 in |
208 in |
209 context |
209 context |
210 |> Data.map (fn (ss, tab) => |
210 |> Data.map (fn (ss, tab) => |