# HG changeset patch
# User blanchet
# Date 1299067797 -3600
# Node ID 9e367f1c95709637a5d72d923d0f8e279744f948
# Parent  a4fb98eb0edf7b72aa3e4535923cd11575d8743c
robust handling of types occurring in "eval" and "preconstr" options but not in the goal

diff -r a4fb98eb0edf -r 9e367f1c9570 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 02 13:09:57 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 02 13:09:57 2011 +0100
@@ -258,16 +258,16 @@
                      o Date.fromTimeLocal o Time.now)
     val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
                 else orig_t
+    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs
     val tfree_table =
-      if merge_type_vars then
-        merged_type_var_table_for_terms thy (neg_t :: assm_ts @ evals)
-      else
-        []
-    val neg_t = merge_type_vars_in_term thy merge_type_vars tfree_table neg_t
-    val assm_ts = map (merge_type_vars_in_term thy merge_type_vars tfree_table)
-                      assm_ts
-    val evals = map (merge_type_vars_in_term thy merge_type_vars tfree_table)
-                    evals
+      if merge_type_vars then merged_type_var_table_for_terms thy conj_ts
+      else []
+    val merge_tfrees = merge_type_vars_in_term thy merge_type_vars tfree_table
+    val neg_t = neg_t |> merge_tfrees
+    val assm_ts = assm_ts |> map merge_tfrees
+    val evals = evals |> map merge_tfrees
+    val preconstrs = preconstrs |> map (apfst (Option.map merge_tfrees))
+    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs
     val original_max_potential = max_potential
     val original_max_genuine = max_genuine
     val max_bisim_depth = fold Integer.max bisim_depths ~1
@@ -299,9 +299,9 @@
        unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
        constr_cache = Unsynchronized.ref []}
     val pseudo_frees = []
-    val real_frees = fold Term.add_frees (neg_t :: assm_ts) []
-    val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
-            raise NOT_SUPPORTED "schematic type variables"
+    val real_frees = fold Term.add_frees conj_ts []
+    val _ = null (fold Term.add_tvars conj_ts []) orelse
+            error "Nitpick cannot handle goals with schematic type variables."
     val (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
          no_poly_user_axioms, binarize) =
       preprocess_formulas hol_ctxt assm_ts neg_t