# HG changeset patch
# User sultana
# Date 1333530265 -3600
# Node ID 360e080fd13e41f03b5a54cc4d7eeec9cb4d6520
# Parent  e9274d23ee28104072e79a3b868c3dffc699e38a
dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret

diff -r e9274d23ee28 -r 360e080fd13e src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- 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