# HG changeset patch
# User wenzelm
# Date 1334959049 -7200
# Node ID 2f7eb28c8b0989686b319ca22ea7b396d1e3b7ac
# Parent  4923b8ba0f49a4a7a4cb20eb442a84e8d83b529b
more standard Theory_Data setup;
keep meta-comments within the history;

diff -r 4923b8ba0f49 -r 2f7eb28c8b09 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- 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