1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 24 16:33:01 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 24 16:43:03 2010 +0200
     1.3 @@ -39,9 +39,6 @@
     1.4      peephole_optim: bool,
     1.5      timeout: Time.time option,
     1.6      tac_timeout: Time.time option,
     1.7 -    sym_break: int,
     1.8 -    sharing_depth: int,
     1.9 -    flatten_props: bool,
    1.10      max_threads: int,
    1.11      show_skolems: bool,
    1.12      show_datatypes: bool,
    1.13 @@ -115,9 +112,6 @@
    1.14    peephole_optim: bool,
    1.15    timeout: Time.time option,
    1.16    tac_timeout: Time.time option,
    1.17 -  sym_break: int,
    1.18 -  sharing_depth: int,
    1.19 -  flatten_props: bool,
    1.20    max_threads: int,
    1.21    show_skolems: bool,
    1.22    show_datatypes: bool,
    1.23 @@ -201,10 +195,9 @@
    1.24           boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
    1.25           verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
    1.26           destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
    1.27 -         fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
    1.28 -         flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
    1.29 -         evals, formats, max_potential, max_genuine, check_potential,
    1.30 -         check_genuine, batch_size, ...} =
    1.31 +         fast_descrs, peephole_optim, tac_timeout, max_threads, show_skolems,
    1.32 +         show_datatypes, show_consts, evals, formats, max_potential,
    1.33 +         max_genuine, check_potential, check_genuine, batch_size, ...} =
    1.34        params
    1.35      val state_ref = Unsynchronized.ref state
    1.36      val pprint =
    1.37 @@ -511,9 +504,9 @@
    1.38          val settings = [("solver", commas_quote kodkod_sat_solver),
    1.39                          ("skolem_depth", "-1"),
    1.40                          ("bit_width", string_of_int bit_width),
    1.41 -                        ("symmetry_breaking", signed_string_of_int sym_break),
    1.42 -                        ("sharing", signed_string_of_int sharing_depth),
    1.43 -                        ("flatten", Bool.toString flatten_props),
    1.44 +                        ("symmetry_breaking", "20"),
    1.45 +                        ("sharing", "3"),
    1.46 +                        ("flatten", "false"),
    1.47                          ("delay", signed_string_of_int delay)]
    1.48          val plain_rels = free_rels @ other_rels
    1.49          val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
    1.50 @@ -922,8 +915,8 @@
    1.51          end
    1.52  
    1.53      val (skipped, the_scopes) =
    1.54 -      all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns
    1.55 -                 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
    1.56 +      all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
    1.57 +                 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
    1.58                   finitizable_dataTs
    1.59      val _ = if skipped > 0 then
    1.60                print_m (fn () => "Too many scopes. Skipping " ^