101 val fTs = map fastype_of rec_fns; |
101 val fTs = map fastype_of rec_fns; |
102 val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T |
102 val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T |
103 (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0))) |
103 (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0))) |
104 (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names); |
104 (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names); |
105 val r = if null is then Extraction.nullt else |
105 val r = if null is then Extraction.nullt else |
106 foldr1 HOLogic.mk_prod (List.mapPartial (fn (((((i, _), T), U), s), tname) => |
106 foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) => |
107 if i mem is then SOME |
107 if i mem is then SOME |
108 (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T)) |
108 (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T)) |
109 else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames)); |
109 else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames)); |
110 val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &") |
110 val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &") |
111 (map (fn ((((i, _), T), U), tname) => |
111 (map (fn ((((i, _), T), U), tname) => |