48 fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) = |
48 fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) = |
49 (map (morph_fp_sugar phi) fp_sugars, |
49 (map (morph_fp_sugar phi) fp_sugars, |
50 (Option.map (morph_lfp_sugar_thms phi) lfp_sugar_thms_opt, |
50 (Option.map (morph_lfp_sugar_thms phi) lfp_sugar_thms_opt, |
51 Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt)); |
51 Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt)); |
52 |
52 |
53 val transfer_n2m_sugar = |
53 val transfer_n2m_sugar = morph_n2m_sugar o Morphism.transfer_morphism; |
54 morph_n2m_sugar o Morphism.transfer_morphism o Proof_Context.theory_of; |
|
55 |
54 |
56 fun n2m_sugar_of ctxt = |
55 fun n2m_sugar_of ctxt = |
57 Typtab.lookup (Data.get (Context.Proof ctxt)) |
56 Typtab.lookup (Data.get (Context.Proof ctxt)) |
58 #> Option.map (transfer_n2m_sugar ctxt); |
57 #> Option.map (transfer_n2m_sugar (Proof_Context.theory_of ctxt)); |
59 |
58 |
60 fun register_n2m_sugar key n2m_sugar = |
59 fun register_n2m_sugar key n2m_sugar = |
61 Local_Theory.declaration {syntax = false, pervasive = false} |
60 Local_Theory.declaration {syntax = false, pervasive = false} |
62 (fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar))); |
61 (fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar))); |
63 |
62 |