src/HOL/Tools/Lifting/lifting_setup.ML
changeset 58928 23d0ffd48006
parent 58903 38c72f5f6c2e
child 59083 88b0b1f28adc
equal deleted inserted replaced
58927:cf47382db395 58928:23d0ffd48006
   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 (Keyword.get_keywords ()) Position.none bundle_name
   224     val pointer = Outer_Syntax.scan (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}