equal
deleted
inserted
replaced
919 ||>> mk_Free "z" (typ_subst_atomic (alphas ~~ typ_pairs) typ_aF) |
919 ||>> mk_Free "z" (typ_subst_atomic (alphas ~~ typ_pairs) typ_aF) |
920 ||>> mk_Frees "ts" typ_pairs |
920 ||>> mk_Frees "ts" typ_pairs |
921 |> fst; |
921 |> fst; |
922 |
922 |
923 (* create local definitions `b = tm` with n arguments *) |
923 (* create local definitions `b = tm` with n arguments *) |
924 fun suffix tm s = (dest_Const tm |> fst |> Long_Name.base_name) ^ s; |
924 fun suffix tm s = Long_Name.base_name (dest_Const_name tm) ^ s; |
925 fun define lthy b n tm = |
925 fun define lthy b n tm = |
926 let |
926 let |
927 val b = Binding.qualify true absT_name (Binding.qualified_name b); |
927 val b = Binding.qualify true absT_name (Binding.qualified_name b); |
928 val ((tm, (_, def)), (lthy, lthy_old)) = lthy |
928 val ((tm, (_, def)), (lthy, lthy_old)) = lthy |
929 |> (snd o Local_Theory.begin_nested) |
929 |> (snd o Local_Theory.begin_nested) |