src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML

--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Feb 17 23:06:24 2016 +0100
@@ -169,7 +169,6 @@
 fun alphanumerated_name prefix name =
   prefix ^ (raw_explode #> map alphanumerate #> implode) name
 
-(*SMLNJ complains if type annotation not used below*)
 fun mk_binding (config : config) ident =
   let
     val pre_binding = Binding.name (alphanumerated_name "bnd_" ident)