# HG changeset patch
# User blanchet
# Date 1394787366 -3600
# Node ID 40f7b45b2472956b666603be9f22f1bffec52046
# Parent  52e8f110fec35a414acb1a60cf5d44116f17184e
made SML/NJ happier

diff -r 52e8f110fec3 -r 40f7b45b2472 src/HOL/Tools/SMT2/z3_new_proof.ML
--- a/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Mar 14 02:54:00 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Mar 14 09:56:06 2014 +0100
@@ -211,7 +211,7 @@
 structure Parsers = Generic_Data
 (
   type T = (int * type_parser) list * (int * term_parser) list
-  val empty = ([(serial (), core_type_parser)], [(serial (), core_term_parser)])
+  val empty : T = ([(serial (), core_type_parser)], [(serial (), core_term_parser)])
   val extend = I
   fun merge ((tys1, ts1), (tys2, ts2)) =
     (Ord_List.merge id_ord (tys1, tys2), Ord_List.merge id_ord (ts1, ts2))