equal
deleted
inserted
replaced
219 (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding |
219 (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding |
220 fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo |
220 fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo |
221 |
221 |
222 val thy = Proof_Context.theory_of lthy |
222 val thy = Proof_Context.theory_of lthy |
223 val dummy_thm = Thm.transfer thy Drule.dummy_thm |
223 val dummy_thm = Thm.transfer thy Drule.dummy_thm |
224 val pointer = Outer_Syntax.scan (Thy_Header.get_keywords thy) Position.none bundle_name |
224 val pointer = Token.explode (Thy_Header.get_keywords thy) Position.none bundle_name |
225 val restore_lifting_att = |
225 val restore_lifting_att = |
226 ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer]) |
226 ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer]) |
227 in |
227 in |
228 lthy |
228 lthy |
229 |> Local_Theory.declaration {syntax = false, pervasive = true} |
229 |> Local_Theory.declaration {syntax = false, pervasive = true} |