src/HOL/Library/Sum_of_Squares/sum_of_squares.ML

    @{term "op ^ :: real => _"}, @{term "abs :: real => _"},
    @{term "min :: real => _"}, @{term "max :: real => _"},
    @{term "0::real"}, @{term "1::real"},
    @{term "numeral :: num => nat"},
    @{term "numeral :: num => real"},
-   @{term "neg_numeral :: num => real"},
    @{term "Num.Bit0"}, @{term "Num.Bit1"}, @{term "Num.One"}];
 
 fun check_sos kcts ct =
  let
   val t = term_of ct