927 fun suffix tm s = (dest_Const tm |> fst |> Long_Name.base_name) ^ s; |
927 fun suffix tm s = (dest_Const tm |> fst |> Long_Name.base_name) ^ s; |
928 fun define lthy b n tm = |
928 fun define lthy b n tm = |
929 let |
929 let |
930 val b = Binding.qualify true absT_name (Binding.qualified_name b); |
930 val b = Binding.qualify true absT_name (Binding.qualified_name b); |
931 val ((tm, (_, def)), (lthy, lthy_old)) = lthy |
931 val ((tm, (_, def)), (lthy, lthy_old)) = lthy |
932 |> Local_Theory.open_target |> snd |
932 |> Local_Theory.open_target |
933 |> Local_Theory.define_internal (((Binding.concealed b, NoSyn), (Binding.empty_atts, tm))) |
933 |> Local_Theory.define_internal (((Binding.concealed b, NoSyn), (Binding.empty_atts, tm))) |
934 ||> `Local_Theory.close_target; |
934 ||> `Local_Theory.close_target; |
935 val phi = Proof_Context.export_morphism lthy_old lthy; |
935 val phi = Proof_Context.export_morphism lthy_old lthy; |
936 val tm = Term.subst_atomic_types |
936 val tm = Term.subst_atomic_types |
937 (map (`(Morphism.typ phi)) (alphas @ betas @ gammas @ map TFree Ds0)) |
937 (map (`(Morphism.typ phi)) (alphas @ betas @ gammas @ map TFree Ds0)) |