# HG changeset patch
# User blanchet
# Date 1284192831 -7200
# Node ID 27f7b7748425e02e0d3c802d8231b20d5c266d10
# Parent  4f9e933a16e2aab480c2ace959c0810b9b5404e7
always handle type variables in typedefs as global

diff -r 4f9e933a16e2 -r 27f7b7748425 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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,