303 unflat (map (fn (_, (_, _, constrs)) => constrs) descr) rec_rewrites; |
303 unflat (map (fn (_, (_, _, constrs)) => constrs) descr) rec_rewrites; |
304 val fvars = rec_rewrites |> hd |> concl_of |> HOLogic.dest_Trueprop |> |
304 val fvars = rec_rewrites |> hd |> concl_of |> HOLogic.dest_Trueprop |> |
305 HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var |> fst; |
305 HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var |> fst; |
306 val (pvars, ctxtvars) = List.partition |
306 val (pvars, ctxtvars) = List.partition |
307 (equal HOLogic.boolT o body_type o snd) |
307 (equal HOLogic.boolT o body_type o snd) |
308 (fold_rev Term.add_vars (map Logic.strip_assums_concl |
308 (subtract (op =) (map dest_Var fvars) (fold_rev Term.add_vars (map Logic.strip_assums_concl |
309 (prems_of (hd rec_rewrites))) [] \\ map dest_Var fvars); |
309 (prems_of (hd rec_rewrites))) [])); |
310 val cfs = defs' |> hd |> snd |> strip_comb |> snd |> |
310 val cfs = defs' |> hd |> snd |> strip_comb |> snd |> |
311 curry (List.take o swap) (length fvars) |> map cert; |
311 curry (List.take o swap) (length fvars) |> map cert; |
312 val invs' = (case invs of |
312 val invs' = (case invs of |
313 NONE => map (fn (i, _) => |
313 NONE => map (fn (i, _) => |
314 Abs ("x", fastype_of (snd (nth defs' i)), HOLogic.true_const)) descr |
314 Abs ("x", fastype_of (snd (nth defs' i)), HOLogic.true_const)) descr |