296 val conj = make_conj ([], []) (map snd conjs) |
296 val conj = make_conj ([], []) (map snd conjs) |
297 |
297 |
298 val (format, type_enc, lam_trans) = |
298 val (format, type_enc, lam_trans) = |
299 (case format_str of |
299 (case format_str of |
300 "FOF" => (FOF, "mono_guards??", liftingN) |
300 "FOF" => (FOF, "mono_guards??", liftingN) |
301 | "TF0" => (TFF Monomorphic, "mono_native", liftingN) |
301 | "TF0" => (TFF (Without_FOOL, Monomorphic), "mono_native", liftingN) |
302 | "TH0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN) |
302 | "TH0" => (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", |
|
303 keep_lamsN) |
303 | "DFG" => (DFG Monomorphic, "mono_native", liftingN) |
304 | "DFG" => (DFG Monomorphic, "mono_native", liftingN) |
304 | _ => error ("Unknown format " ^ quote format_str ^ |
305 | _ => error ("Unknown format " ^ quote format_str ^ |
305 " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")")) |
306 " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")")) |
306 val generate_info = false |
307 val generate_info = false |
307 val uncurried_aliases = false |
308 val uncurried_aliases = false |