equal
deleted
inserted
replaced
917 val (skipped, the_scopes) = |
917 val (skipped, the_scopes) = |
918 all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns |
918 all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns |
919 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs |
919 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs |
920 finitizable_dataTs |
920 finitizable_dataTs |
921 val _ = if skipped > 0 then |
921 val _ = if skipped > 0 then |
922 print_nt (fn () => "Too many scopes. Skipping " ^ |
922 print_nt (fn () => "Skipping " ^ string_of_int skipped ^ |
923 string_of_int skipped ^ " scope" ^ |
923 " scope" ^ plural_s skipped ^ |
924 plural_s skipped ^ |
|
925 ". (Consider using \"mono\" or \ |
924 ". (Consider using \"mono\" or \ |
926 \\"merge_type_vars\" to prevent this.)") |
925 \\"merge_type_vars\" to prevent this.)") |
927 else |
926 else |
928 () |
927 () |
929 val _ = scopes := the_scopes |
928 val _ = scopes := the_scopes |