--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 04 10:49:42 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 04 10:04:25 2012 +0100
@@ -178,7 +178,8 @@
(type T = manifest list
val empty = []
val extend = I
- val merge = Library.merge (op =))
+ (*SMLNJ complains if non-expanded form used below*)
+ fun merge v = Library.merge (op =) v)
val get_manifests = TPTP_Data.get
@@ -189,7 +190,8 @@
val IND_TYPE = "ind"
-fun mk_binding config ident =
+(*SMLNJ complains if type annotation not used below*)
+fun mk_binding (config : config) ident =
let
val pre_binding = Binding.name ident
in