--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Sep 10 23:56:35 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Sep 11 10:13:51 2010 +0200
@@ -595,9 +595,13 @@
else case Typedef.get_info ctxt s of
(* When several entries are returned, it shouldn't matter much which one
we take (according to Florian Haftmann). *)
+ (* The "Logic.varifyT_global" calls are a temporary hack because these
+ types's type variables sometimes clash with locally fixed type variables.
+ Remove these calls once "Typedef" is fully localized. *)
({abs_type, rep_type, Abs_name, Rep_name, ...},
{set_def, Rep, Abs_inverse, Rep_inverse, ...}) :: _ =>
- SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
+ SOME {abs_type = Logic.varifyT_global abs_type,
+ rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name,
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
Rep_inverse = SOME Rep_inverse}
@@ -1567,7 +1571,7 @@
| [_, (@{const True}, head_t2)] => head_t2
| [_, (@{const False}, head_t2)] => @{const Not} $ head_t2
| _ => raise BAD ("Nitpick_HOL.optimized_case_def", "impossible cases")
- else
+ else
@{const True} |> fold_rev (add_constr_case res_T) cases
else
fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
@@ -1748,7 +1752,7 @@
val rep_T = domain_type (domain_type T)
val eps_fun = Const (@{const_name Eps},
(rep_T --> bool_T) --> rep_T)
- val normal_fun =
+ val normal_fun =
Const (quot_normal_name_for_type ctxt abs_T,
rep_T --> rep_T)
val abs_fun = Const (@{const_name Quot}, rep_T --> abs_T)
@@ -2163,7 +2167,7 @@
(disjuncts_of body)
val base_body = nonrecs |> List.foldl s_disj @{const False}
val step_body = recs |> map (repair_rec j)
- |> List.foldl s_disj @{const False}
+ |> List.foldl s_disj @{const False}
in
(list_abs (tl xs, incr_bv (~1, j, base_body))
|> ap_n_split (length arg_Ts) tuple_T bool_T,