--- a/src/Tools/nbe.ML Tue Jun 30 16:43:27 2009 +0200
+++ b/src/Tools/nbe.ML Tue Jun 30 16:43:28 2009 +0200
@@ -135,6 +135,8 @@
| nbe_fun i c = "c_" ^ translate_string (fn "." => "_" | c => c) c ^ "_" ^ string_of_int i;
fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
fun nbe_bound v = "v_" ^ v;
+fun nbe_bound_optional NONE = "_"
+ | nbe_bound_optional (SOME v) = nbe_bound v;
fun nbe_default v = "w_" ^ v;
(*note: these three are the "turning spots" where proper argument order is established!*)
@@ -193,7 +195,7 @@
and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
| of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
| of_iapp match_cont ((v, _) `|=> t) ts =
- nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts
+ nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
| of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
nbe_apps (ml_cases (of_iterm NONE t)
(map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs