--- a/src/HOL/Nominal/nominal_datatype.ML Thu Dec 15 13:40:20 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Dec 15 14:11:57 2011 +0100
@@ -858,14 +858,14 @@
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) =
+ fun prove_distinct_thms _ [] = []
+ | prove_distinct_thms (p as (rep_thms, dist_lemma)) (t :: ts) =
let
val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
in
dist_thm :: Drule.export_without_context (dist_thm RS not_sym) ::
- prove_distinct_thms p (k, ts)
+ prove_distinct_thms p ts
end;
val distinct_thms = map2 prove_distinct_thms
--- a/src/HOL/Tools/Datatype/datatype.ML Thu Dec 15 13:40:20 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Thu Dec 15 14:11:57 2011 +0100
@@ -211,7 +211,7 @@
(* constructor definitions *)
- fun make_constr_def tname (typedef: Typedef.info) T n
+ fun make_constr_def (typedef: Typedef.info) T n
((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
let
fun constr_arg dt (j, l_args, r_args) =
@@ -257,7 +257,7 @@
Drule.export_without_context
(cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
val (thy', defs', eqns', _) =
- fold (make_constr_def tname typedef T (length constrs))
+ fold (make_constr_def typedef T (length constrs))
(constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
in
(Sign.parent_path thy', defs', eqns @ [eqns'],
@@ -534,7 +534,7 @@
dist_lemma :: (rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
(constr_rep_thms ~~ dist_lemmas);
- fun prove_distinct_thms dist_rewrites' (k, ts) =
+ fun prove_distinct_thms dist_rewrites' =
let
fun prove [] = []
| prove (t :: ts) =
@@ -542,7 +542,7 @@
val dist_thm = Skip_Proof.prove_global thy5 [] [] t (fn _ =>
EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
in dist_thm :: Drule.export_without_context (dist_thm RS not_sym) :: prove ts end;
- in prove ts end;
+ in prove end;
val distinct_thms =
map2 (prove_distinct_thms) dist_rewrites (Datatype_Prop.make_distincts descr);
@@ -734,9 +734,9 @@
[] => ()
| dups => error ("Duplicate datatypes: " ^ commas_quote dups));
- fun prep_dt_spec ((tname, tvs, mx), constrs) (dts', constr_syntax, i) =
+ fun prep_dt_spec ((tname, tvs, _), constrs) (dts', constr_syntax, i) =
let
- fun prep_constr (cname, cargs, mx') (constrs, constr_syntax') =
+ fun prep_constr (cname, cargs, mx) (constrs, constr_syntax') =
let
val _ =
(case subtract (op =) tvs (fold Term.add_tfreesT cargs []) of
@@ -745,7 +745,7 @@
val c = Sign.full_name_path thy (Binding.name_of tname) cname;
in
(constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs)],
- constr_syntax' @ [(cname, mx')])
+ constr_syntax' @ [(cname, mx)])
end handle ERROR msg =>
cat_error msg ("The error above occurred in constructor " ^ Binding.print cname ^
" of datatype " ^ Binding.print tname);
--- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Dec 15 13:40:20 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Thu Dec 15 14:11:57 2011 +0100
@@ -72,7 +72,7 @@
(*Produce an instance of a constructor, plus fresh variables for its arguments.*)
fun fresh_constr ty_match ty_inst colty used c =
let
- val (_, Ty) = dest_Const c
+ val (_, Ty) = dest_Const c;
val Ts = binder_types Ty;
val names =
Name.variant_list used (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
@@ -84,7 +84,7 @@
in (c', gvars) end;
-(*Goes through a list of rows and picks out the ones beginning with a
+(*Go through a list of rows and pick out the ones beginning with a
pattern with constructor = name.*)
fun mk_group (name, T) rows =
let val k = length (binder_types T) in
@@ -203,14 +203,16 @@
fun case_error s = error ("Error in case expression:\n" ^ s);
+local
+
(*Repeated variable occurrences in a pattern are not allowed.*)
fun no_repeat_vars ctxt pat = fold_aterms
(fn x as Free (s, _) =>
- (fn xs =>
- if member op aconv xs x then
- case_error (quote s ^ " occurs repeatedly in the pattern " ^
- quote (Syntax.string_of_term ctxt pat))
- else x :: xs)
+ (fn xs =>
+ if member op aconv xs x then
+ case_error (quote s ^ " occurs repeatedly in the pattern " ^
+ quote (Syntax.string_of_term ctxt pat))
+ else x :: xs)
| _ => I) pat [];
fun gen_make_case ty_match ty_inst type_of tab ctxt config used x clauses =
@@ -241,6 +243,8 @@
case_tm
end;
+in
+
fun make_case tab ctxt =
gen_make_case (match_type (Proof_Context.theory_of ctxt))
Envir.subst_term_types fastype_of tab ctxt;
@@ -248,6 +252,8 @@
val make_case_untyped =
gen_make_case (K (K Vartab.empty)) (K (Term.map_types (K dummyT))) (K dummyT);
+end;
+
(* parse translation *)
@@ -297,6 +303,8 @@
(* destruct one level of pattern matching *)
+local
+
(* FIXME proper name context!? *)
fun gen_dest_case name_of type_of tab d used t =
(case apfst name_of (strip_comb t) of
@@ -362,12 +370,18 @@
end
| _ => NONE);
+in
+
val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
val dest_case' = gen_dest_case (try (dest_Const #> fst #> Lexicon.unmark_const)) (K dummyT);
+end;
+
(* destruct nested patterns *)
+local
+
fun strip_case'' dest (pat, rhs) =
(case dest (Term.add_free_names pat []) rhs of
SOME (exp as Free _, clauses) =>
@@ -385,9 +399,13 @@
SOME (x, clauses) => SOME (x, maps (strip_case'' dest) clauses)
| NONE => NONE);
+in
+
val strip_case = gen_strip_case oo dest_case;
val strip_case' = gen_strip_case oo dest_case';
+end;
+
(* print translation *)
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Dec 15 13:40:20 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Dec 15 14:11:57 2011 +0100
@@ -79,8 +79,7 @@
val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr]) index);
fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
[trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
- val distincts =
- maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr]) index));
+ val distincts = maps prep_distinct (nth (Datatype_Prop.make_distincts [descr]) index);
val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
val simpset =
Simplifier.global_context thy
--- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Dec 15 13:40:20 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Dec 15 14:11:57 2011 +0100
@@ -413,7 +413,7 @@
(i, (tyco, map Datatype_Aux.DtTFree vs, (map o apsnd) dtyps_of_typ constr));
val descr = map_index mk_spec cs;
val injs = Datatype_Prop.make_injs [descr];
- val half_distincts = map snd (Datatype_Prop.make_distincts [descr]);
+ val half_distincts = Datatype_Prop.make_distincts [descr];
val ind = Datatype_Prop.make_ind [descr];
val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts];
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Dec 15 13:40:20 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Dec 15 14:11:57 2011 +0100
@@ -10,7 +10,7 @@
val indexify_names: string list -> string list
val make_tnames: typ list -> string list
val make_injs : descr list -> term list list
- val make_distincts : descr list -> (int * term list) list (*no symmetric inequalities*)
+ val make_distincts : descr list -> term list list (*no symmetric inequalities*)
val make_ind : descr list -> term
val make_casedists : descr list -> term list
val make_primrec_Ts : descr list -> string list -> typ list * typ list
@@ -99,7 +99,7 @@
in map make_distincts'' constrs @ make_distincts' T constrs end;
in
map2 (fn ((_, (_, _, constrs))) => fn T =>
- (length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs
+ make_distincts' T (map prep_constr constrs)) (hd descr) newTs
end;