equal
deleted
inserted
replaced
130 {name = Local_Theory.full_name lthy b, |
130 {name = Local_Theory.full_name lthy b, |
131 lhss = |
131 lhss = |
132 let |
132 let |
133 val lhss' = prep lthy lhss; |
133 val lhss' = prep lthy lhss; |
134 val ctxt' = fold Variable.auto_fixes lhss' lthy; |
134 val ctxt' = fold Variable.auto_fixes lhss' lthy; |
135 in Variable.export_terms ctxt' lthy lhss' end |
135 in Variable.export_terms ctxt' lthy lhss' end |> map (Proof_Context.cterm_of lthy), |
136 |> map (Thm.cterm_of (Proof_Context.theory_of lthy)), |
|
137 proc = proc, |
136 proc = proc, |
138 identifier = identifier}; |
137 identifier = identifier}; |
139 in |
138 in |
140 lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => |
139 lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => |
141 let |
140 let |