# HG changeset patch
# User boehmes
# Date 1260294252 -3600
# Node ID 687140d426e9e22c77af29cda1c4f50c590f7520
# Parent  7996b488a9b509a3019531a9f71076a28e91c78b
made SML/NJ happy

diff -r 7996b488a9b5 -r 687140d426e9 src/HOL/SMT/Tools/smt_translate.ML
--- a/src/HOL/SMT/Tools/smt_translate.ML	Mon Dec 07 23:06:03 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_translate.ML	Tue Dec 08 18:44:12 2009 +0100
@@ -284,7 +284,7 @@
     | mark f false t = f false t #>> app formula_marker o single
   fun mark' f false t = f true t #>> app term_marker o single
     | mark' f true t = f true t
-  val mark_term = app term_marker o single
+  fun mark_term (t : (sym, typ) sterm) = app term_marker [t]
   fun lift_term_marker c ts =
     let val rem = (fn SApp (SConst (@{const_name term}, _), [t]) => t | t => t)
     in mark_term (SApp (c, map rem ts)) end