equal
deleted
inserted
replaced
387 | postprocess_subterms Ts (Abs (s, T, t')) = |
387 | postprocess_subterms Ts (Abs (s, T, t')) = |
388 Abs (s, T, postprocess_subterms (T :: Ts) t') |
388 Abs (s, T, postprocess_subterms (T :: Ts) t') |
389 | postprocess_subterms Ts t = postprocess_term (fastype_of1 (Ts, t)) t |
389 | postprocess_subterms Ts t = postprocess_term (fastype_of1 (Ts, t)) t |
390 fun make_set maybe_opt T tps = |
390 fun make_set maybe_opt T tps = |
391 let |
391 let |
392 val empty_const = Const (@{const_abbrev Set.empty}, T --> bool_T) |
392 val set_T = HOLogic.mk_setT T |
393 val insert_const = |
393 val empty_const = Const (@{const_abbrev Set.empty}, set_T) |
394 Const (@{const_name insert}, T --> (T --> bool_T) --> T --> bool_T) |
394 val insert_const = Const (@{const_name insert}, T --> set_T --> set_T) |
395 fun aux [] = |
395 fun aux [] = |
396 if maybe_opt andalso not (is_complete_type datatypes false T) then |
396 if maybe_opt andalso not (is_complete_type datatypes false T) then |
397 insert_const $ Const (unrep (), T) $ empty_const |
397 insert_const $ Const (unrep (), T) $ empty_const |
398 else |
398 else |
399 empty_const |
399 empty_const |
406 ? curry (op $) |
406 ? curry (op $) |
407 (Const (maybe_name, T --> T)))) |
407 (Const (maybe_name, T --> T)))) |
408 in |
408 in |
409 if forall (fn (_, t) => t <> @{const True} andalso t <> @{const False}) |
409 if forall (fn (_, t) => t <> @{const True} andalso t <> @{const False}) |
410 tps then |
410 tps then |
411 Const (unknown, T --> bool_T) |
411 Const (unknown, set_T) |
412 else |
412 else |
413 aux tps |
413 aux tps |
414 end |
414 end |
415 fun make_map maybe_opt T1 T2 T2' = |
415 fun make_map maybe_opt T1 T2 T2' = |
416 let |
416 let |