src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML

        val SOME den = Int.fromString (String.substring(s,n+1,String.size s - n - 1))
    in rat_of_quotient(numer, den)
    end
  end;
 
-fun isspace x = x = " " ;
-fun isnum x = x mem_string ["0","1","2","3","4","5","6","7","8","9"]
+fun isspace x = (x = " ");
+fun isnum x = member (op =) ["0","1","2","3","4","5","6","7","8","9"] x;
 
 (* More parser basics.                                                       *)
 
  val word = Scan.this_string
  fun token s =