equal
deleted
inserted
replaced
1938 | (t, Term Output) => NONE |
1938 | (t, Term Output) => NONE |
1939 | (Const (name, T), Context mode) => |
1939 | (Const (name, T), Context mode) => |
1940 (case alternative_function_of (ProofContext.theory_of ctxt) name mode of |
1940 (case alternative_function_of (ProofContext.theory_of ctxt) name mode of |
1941 SOME alt_function_name => |
1941 SOME alt_function_name => |
1942 let |
1942 let |
1943 val (inpTs, outpTs) = split_modeT' mode (binder_types T) |
1943 val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) |
|
1944 mode (binder_types T) |
1944 val bs = map (pair "x") inpTs |
1945 val bs = map (pair "x") inpTs |
1945 val bounds = map Bound (rev (0 upto (length bs) - 1)) |
1946 val bounds = map Bound (rev (0 upto (length bs) - 1)) |
1946 val f = Const (alt_function_name, inpTs ---> HOLogic.mk_tupleT outpTs) |
1947 val f = Const (alt_function_name, inpTs ---> HOLogic.mk_tupleT outpTs) |
1947 in SOME (list_abs (bs, mk_single compfuns (list_comb (f, bounds)))) end |
1948 in SOME (list_abs (bs, mk_single compfuns (list_comb (f, bounds)))) end |
1948 | NONE => |
1949 | NONE => |