--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Apr 20 23:34:03 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Apr 20 23:57:29 2012 +0200
@@ -150,12 +150,14 @@
(type_map * const_map * tptp_formula_meaning list)
type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning
+
structure TPTP_Data = Theory_Data
- (type T = manifest list
- val empty = []
- val extend = I
- (*SMLNJ complains if non-expanded form used below*)
- fun merge v = Library.merge (op =) v)
+(
+ type T = manifest list
+ val empty = []
+ val extend = I
+ fun merge data : T = Library.merge (op =) data
+)
val get_manifests = TPTP_Data.get