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