340 fun mk_reporting_generator_expr thy prop Ts = |
340 fun mk_reporting_generator_expr thy prop Ts = |
341 let |
341 let |
342 val bound_max = length Ts - 1; |
342 val bound_max = length Ts - 1; |
343 val bounds = map_index (fn (i, ty) => |
343 val bounds = map_index (fn (i, ty) => |
344 (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts; |
344 (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts; |
345 fun strip_imp (Const("op -->",_) $ A $ B) = apfst (cons A) (strip_imp B) |
345 fun strip_imp (Const(@{const_name "op -->"},_) $ A $ B) = apfst (cons A) (strip_imp B) |
346 | strip_imp A = ([], A) |
346 | strip_imp A = ([], A) |
347 val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds); |
347 val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds); |
348 val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds) |
348 val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds) |
349 val (assms, concl) = strip_imp prop' |
349 val (assms, concl) = strip_imp prop' |
350 val return = |
350 val return = |