# HG changeset patch
# User blanchet
# Date 1275399800 -7200
# Node ID 9f2c3d3c8f0fca93d2f09b947182f7e03a1b46e5
# Parent  8b931fb51cc67854fe72816f411c245f1f123351
remove debug output

diff -r 8b931fb51cc6 -r 9f2c3d3c8f0f src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jun 01 15:38:47 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jun 01 15:43:20 2010 +0200
@@ -608,7 +608,6 @@
       | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
                      (Func (R1, Formula Neut)) jss =
         let
-val _ = priority ("HERE: " ^ (if maybe_opt then "y" else "n")) (* ### *)
           val jss1 = all_combinations_for_rep R1
           val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
           val ts2 =