equal
deleted
inserted
replaced
1045 fun print_failed_mode options thy modes p m rs i = |
1045 fun print_failed_mode options thy modes p m rs i = |
1046 if show_mode_inference options then |
1046 if show_mode_inference options then |
1047 let |
1047 let |
1048 val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^ |
1048 val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^ |
1049 p ^ " violates mode " ^ string_of_mode thy p m) |
1049 p ^ " violates mode " ^ string_of_mode thy p m) |
1050 val _ = tracing (string_of_clause thy p (nth rs i)) |
|
1051 in () end |
1050 in () end |
1052 else () |
1051 else () |
1053 |
1052 |
1054 fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) = |
1053 fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) = |
1055 let |
1054 let |