# HG changeset patch
# User blanchet
# Date 1299067797 -3600
# Node ID a14a492f472f11f84ea79333c47f4d431100c756
# Parent  9e367f1c95709637a5d72d923d0f8e279744f948
unfold definitions in "preconstrs" option

diff -r 9e367f1c9570 -r a14a492f472f src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Mar 02 13:09:57 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Mar 02 13:09:57 2011 +0100
@@ -1284,7 +1284,9 @@
     val preconstr_ts =
       (* FIXME: Implement preconstruction inference. *)
       preconstrs
-      |> map_filter (fn (SOME t, SOME true) => SOME (t |> do_middle false)
+      |> map_filter (fn (SOME t, SOME true) =>
+                        SOME (t |> unfold_defs_in_term hol_ctxt
+                                |> do_middle false)
                       | _ => NONE)
     val nondef_ts = nondef_ts |> map (do_tail false)
     val def_ts = def_ts |> map (do_middle true #> do_tail true)