--- 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))