changeset 2477 | 2f289c1f6cf1 |
parent 2476 | 8f8652a8107f |
child 2480 | ac7dff1194e8 |
--- a/Nominal/nominal_dt_alpha.ML Sat Sep 11 05:56:49 2010 +0800 +++ b/Nominal/nominal_dt_alpha.ML Sun Sep 12 22:46:40 2010 +0800 @@ -371,7 +371,8 @@ val true_trms = replicate (length alphas) (K @{term True}) fun apply_all x fs = map (fn f => f x) fs - val goals_rhs = + + val goals_rhs = group (props @ (alphas ~~ true_trms)) |> map snd |> map2 apply_all (args1 ~~ args2)