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