made SML/NJ happier
authorblanchet
Fri Mar 14 09:56:06 2014 +0100 (2014-03-14)
changeset 5612240f7b45b2472
parent 56121 52e8f110fec3
child 56123 a27859b0ef7d
made SML/NJ happier
src/HOL/Tools/SMT2/z3_new_proof.ML
     1.1 --- a/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Mar 14 02:54:00 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Mar 14 09:56:06 2014 +0100
     1.3 @@ -211,7 +211,7 @@
     1.4  structure Parsers = Generic_Data
     1.5  (
     1.6    type T = (int * type_parser) list * (int * term_parser) list
     1.7 -  val empty = ([(serial (), core_type_parser)], [(serial (), core_term_parser)])
     1.8 +  val empty : T = ([(serial (), core_type_parser)], [(serial (), core_term_parser)])
     1.9    val extend = I
    1.10    fun merge ((tys1, ts1), (tys2, ts2)) =
    1.11      (Ord_List.merge id_ord (tys1, tys2), Ord_List.merge id_ord (ts1, ts2))