equal
deleted
inserted
replaced
369 val args2 = map2 (curry Free) arg_names2 arg_tys |
369 val args2 = map2 (curry Free) arg_names2 arg_tys |
370 |
370 |
371 val true_trms = replicate (length alphas) (K @{term True}) |
371 val true_trms = replicate (length alphas) (K @{term True}) |
372 |
372 |
373 fun apply_all x fs = map (fn f => f x) fs |
373 fun apply_all x fs = map (fn f => f x) fs |
374 val goals_rhs = |
374 |
|
375 val goals_rhs = |
375 group (props @ (alphas ~~ true_trms)) |
376 group (props @ (alphas ~~ true_trms)) |
376 |> map snd |
377 |> map snd |
377 |> map2 apply_all (args1 ~~ args2) |
378 |> map2 apply_all (args1 ~~ args2) |
378 |> map fold_conj |
379 |> map fold_conj |
379 |
380 |