| changeset 47108 | 2a1953f0d20d |
| parent 46243 | 4b1b43ab7c62 |
| child 47490 | f4348634595b |
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Mar 24 16:27:04 2012 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Mar 25 20:15:39 2012 +0200 @@ -206,7 +206,7 @@ val syntactic_sorts = @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @ - @{sort number} + @{sort numeral} fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) = subset (op =) (S, syntactic_sorts) | has_tfree_syntactic_sort _ = false