--- a/src/HOL/Nominal/nominal_package.ML Fri May 23 16:05:02 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Fri May 23 16:05:04 2008 +0200
@@ -850,26 +850,22 @@
(* prove distinctness theorems *)
- val distinctness_limit = Config.get_thy thy8 DatatypeProp.distinctness_limit;
- val thy8' = Config.put_thy DatatypeProp.distinctness_limit 1000 thy8;
- val distinct_props = DatatypeProp.make_distincts new_type_names descr' sorts' thy8';
- val thy8 = Config.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8';
-
+ 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);
- fun prove_distinct_thms (_, []) = []
- | prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) =
+ 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, ts))
+ in dist_thm :: (standard (dist_thm RS not_sym)) ::
+ (prove_distinct_thms p (k, ts))
end;
- val distinct_thms = map prove_distinct_thms
- (constr_rep_thmss ~~ dist_lemmas ~~ distinct_props);
+ val distinct_thms = map2 prove_distinct_thms
+ (constr_rep_thmss ~~ dist_lemmas) distinct_props;
(** prove equations for permutation functions **)