--- a/src/HOL/Nominal/nominal_package.ML Fri Jun 20 21:00:21 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Fri Jun 20 21:00:22 2008 +0200
@@ -844,17 +844,17 @@
(* prove distinctness theorems *)
val distinct_props = DatatypeProp.make_distincts descr' sorts';
- val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
- dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
- (constr_rep_thmss ~~ dist_lemmas);
+ val dist_rewrites = map2 (fn rep_thms => fn dist_lemma =>
+ dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])
+ constr_rep_thmss dist_lemmas;
fun prove_distinct_thms _ (_, []) = []
| prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) =
let
val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
- in dist_thm :: (standard (dist_thm RS not_sym)) ::
- (prove_distinct_thms p (k, ts))
+ in dist_thm :: standard (dist_thm RS not_sym) ::
+ prove_distinct_thms p (k, ts)
end;
val distinct_thms = map2 prove_distinct_thms