author | blanchet |
Tue, 01 Jun 2010 15:43:20 +0200 | |
changeset 37265 | 9f2c3d3c8f0f |
parent 37264 | 8b931fb51cc6 |
child 37266 | 773dc74118f6 |
--- 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 =