# HG changeset patch
# User boehmes
# Date 1260294445 -3600
# Node ID 28dae2b40c6fa4c08359cffe7dc2d36ae405d05b
# Parent  687140d426e9e22c77af29cda1c4f50c590f7520# Parent  f13b5c023e656c5312f8aba6dfe6b972118e1665
merged

diff -r f13b5c023e65 -r 28dae2b40c6f src/HOL/SMT/Tools/smt_translate.ML
--- a/src/HOL/SMT/Tools/smt_translate.ML	Tue Dec 08 14:31:19 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_translate.ML	Tue Dec 08 18:47:25 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