# HG changeset patch
# User blanchet
# Date 1272147944 -7200
# Node ID eee4ee6a5cbe55906f68f7d5fda8aa806d382434
# Parent  8228b3a4a2baca7c53001488eb15109b1ceb5ef7
remove "show_skolems" option and change style of record declarations

diff -r 8228b3a4a2ba -r eee4ee6a5cbe doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Sun Apr 25 00:10:30 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Sun Apr 25 00:25:44 2010 +0200
@@ -2190,12 +2190,6 @@
 {\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
 \textit{batch\_size} (\S\ref{optimizations}).}
 
-\optrue{show\_skolems}{hide\_skolem}
-Specifies whether the values of Skolem constants should be displayed as part of
-counterexamples. Skolem constants correspond to bound variables in the original
-formula and usually help us to understand why the counterexample falsifies the
-formula.
-
 \opfalse{show\_datatypes}{hide\_datatypes}
 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
 be displayed as part of counterexamples. Such subsets are sometimes helpful when
@@ -2209,8 +2203,8 @@
 genuine, but they can clutter the output.
 
 \opfalse{show\_all}{dont\_show\_all}
-Enabling this option effectively enables \textit{show\_skolems},
-\textit{show\_datatypes}, and \textit{show\_consts}.
+Enabling this option effectively enables \textit{show\_datatypes} and
+\textit{show\_consts}.
 
 \opdefault{max\_potential}{int}{$\mathbf{1}$}
 Specifies the maximum number of potential counterexamples to display. Setting
diff -r 8228b3a4a2ba -r eee4ee6a5cbe src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/HISTORY	Sun Apr 25 00:25:44 2010 +0200
@@ -17,8 +17,8 @@
   * Added cache to speed up repeated Kodkod invocations on the same problems
   * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
     "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
-  * Removed "skolemize", "uncurry", "sym_break", "flatten_prop", and
-    "sharing_depth" options
+  * Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
+    "sharing_depth", and "show_skolems" options
 
 Version 2009-1
 
diff -r 8228b3a4a2ba -r eee4ee6a5cbe src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sun Apr 25 00:25:44 2010 +0200
@@ -120,11 +120,10 @@
     AssignRelReg of n_ary_index * rel_expr |
     AssignIntReg of int * int_expr
 
-  type 'a fold_expr_funcs = {
-    formula_func: formula -> 'a -> 'a,
-    rel_expr_func: rel_expr -> 'a -> 'a,
-    int_expr_func: int_expr -> 'a -> 'a
-  }
+  type 'a fold_expr_funcs =
+    {formula_func: formula -> 'a -> 'a,
+     rel_expr_func: rel_expr -> 'a -> 'a,
+     int_expr_func: int_expr -> 'a -> 'a}
 
   val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a
   val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a
@@ -132,10 +131,9 @@
   val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a
   val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a
 
-  type 'a fold_tuple_funcs = {
-    tuple_func: tuple -> 'a -> 'a,
-    tuple_set_func: tuple_set -> 'a -> 'a
-  }
+  type 'a fold_tuple_funcs =
+    {tuple_func: tuple -> 'a -> 'a,
+     tuple_set_func: tuple_set -> 'a -> 'a}
 
   val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a
   val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a
@@ -144,15 +142,15 @@
       'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a
   val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a
 
-  type problem = {
-    comment: string,
-    settings: setting list,
-    univ_card: int,
-    tuple_assigns: tuple_assign list,
-    bounds: bound list,
-    int_bounds: int_bound list,
-    expr_assigns: expr_assign list,
-    formula: formula}
+  type problem =
+    {comment: string,
+     settings: setting list,
+     univ_card: int,
+     tuple_assigns: tuple_assign list,
+     bounds: bound list,
+     int_bounds: int_bound list,
+     expr_assigns: expr_assign list,
+     formula: formula}
 
   type raw_bound = n_ary_index * int list list
 
@@ -291,15 +289,15 @@
   AssignRelReg of n_ary_index * rel_expr |
   AssignIntReg of int * int_expr
 
-type problem = {
-  comment: string,
-  settings: setting list,
-  univ_card: int,
-  tuple_assigns: tuple_assign list,
-  bounds: bound list,
-  int_bounds: int_bound list,
-  expr_assigns: expr_assign list,
-  formula: formula}
+type problem =
+  {comment: string,
+   settings: setting list,
+   univ_card: int,
+   tuple_assigns: tuple_assign list,
+   bounds: bound list,
+   int_bounds: int_bound list,
+   expr_assigns: expr_assign list,
+   formula: formula}
 
 type raw_bound = n_ary_index * int list list
 
@@ -313,11 +311,10 @@
 
 exception SYNTAX of string * string
 
-type 'a fold_expr_funcs = {
-  formula_func: formula -> 'a -> 'a,
-  rel_expr_func: rel_expr -> 'a -> 'a,
-  int_expr_func: int_expr -> 'a -> 'a
-}
+type 'a fold_expr_funcs =
+  {formula_func: formula -> 'a -> 'a,
+   rel_expr_func: rel_expr -> 'a -> 'a,
+   int_expr_func: int_expr -> 'a -> 'a}
 
 (** Auxiliary functions on ML representation of Kodkod problems **)
 
@@ -419,10 +416,9 @@
   | AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r
   | AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i
 
-type 'a fold_tuple_funcs = {
-  tuple_func: tuple -> 'a -> 'a,
-  tuple_set_func: tuple_set -> 'a -> 'a
-}
+type 'a fold_tuple_funcs =
+  {tuple_func: tuple -> 'a -> 'a,
+   tuple_set_func: tuple_set -> 'a -> 'a}
 
 fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F
 fun fold_tuple_set F tuple_set =
diff -r 8228b3a4a2ba -r eee4ee6a5cbe src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Apr 25 00:25:44 2010 +0200
@@ -9,46 +9,45 @@
 sig
   type styp = Nitpick_Util.styp
   type term_postprocessor = Nitpick_Model.term_postprocessor
-  type params = {
-    cards_assigns: (typ option * int list) list,
-    maxes_assigns: (styp option * int list) list,
-    iters_assigns: (styp option * int list) list,
-    bitss: int list,
-    bisim_depths: int list,
-    boxes: (typ option * bool option) list,
-    finitizes: (typ option * bool option) list,
-    monos: (typ option * bool option) list,
-    stds: (typ option * bool) list,
-    wfs: (styp option * bool option) list,
-    sat_solver: string,
-    blocking: bool,
-    falsify: bool,
-    debug: bool,
-    verbose: bool,
-    overlord: bool,
-    user_axioms: bool option,
-    assms: bool,
-    merge_type_vars: bool,
-    binary_ints: bool option,
-    destroy_constrs: bool,
-    specialize: bool,
-    star_linear_preds: bool,
-    fast_descrs: bool,
-    peephole_optim: bool,
-    timeout: Time.time option,
-    tac_timeout: Time.time option,
-    max_threads: int,
-    show_skolems: bool,
-    show_datatypes: bool,
-    show_consts: bool,
-    evals: term list,
-    formats: (term option * int list) list,
-    max_potential: int,
-    max_genuine: int,
-    check_potential: bool,
-    check_genuine: bool,
-    batch_size: int,
-    expect: string}
+  type params =
+    {cards_assigns: (typ option * int list) list,
+     maxes_assigns: (styp option * int list) list,
+     iters_assigns: (styp option * int list) list,
+     bitss: int list,
+     bisim_depths: int list,
+     boxes: (typ option * bool option) list,
+     finitizes: (typ option * bool option) list,
+     monos: (typ option * bool option) list,
+     stds: (typ option * bool) list,
+     wfs: (styp option * bool option) list,
+     sat_solver: string,
+     blocking: bool,
+     falsify: bool,
+     debug: bool,
+     verbose: bool,
+     overlord: bool,
+     user_axioms: bool option,
+     assms: bool,
+     merge_type_vars: bool,
+     binary_ints: bool option,
+     destroy_constrs: bool,
+     specialize: bool,
+     star_linear_preds: bool,
+     fast_descrs: bool,
+     peephole_optim: bool,
+     timeout: Time.time option,
+     tac_timeout: Time.time option,
+     max_threads: int,
+     show_datatypes: bool,
+     show_consts: bool,
+     evals: term list,
+     formats: (term option * int list) list,
+     max_potential: int,
+     max_genuine: int,
+     check_potential: bool,
+     check_genuine: bool,
+     batch_size: int,
+     expect: string}
 
   val register_frac_type : string -> (string * string) list -> theory -> theory
   val unregister_frac_type : string -> theory -> theory
@@ -80,55 +79,54 @@
 
 structure KK = Kodkod
 
-type params = {
-  cards_assigns: (typ option * int list) list,
-  maxes_assigns: (styp option * int list) list,
-  iters_assigns: (styp option * int list) list,
-  bitss: int list,
-  bisim_depths: int list,
-  boxes: (typ option * bool option) list,
-  finitizes: (typ option * bool option) list,
-  monos: (typ option * bool option) list,
-  stds: (typ option * bool) list,
-  wfs: (styp option * bool option) list,
-  sat_solver: string,
-  blocking: bool,
-  falsify: bool,
-  debug: bool,
-  verbose: bool,
-  overlord: bool,
-  user_axioms: bool option,
-  assms: bool,
-  merge_type_vars: bool,
-  binary_ints: bool option,
-  destroy_constrs: bool,
-  specialize: bool,
-  star_linear_preds: bool,
-  fast_descrs: bool,
-  peephole_optim: bool,
-  timeout: Time.time option,
-  tac_timeout: Time.time option,
-  max_threads: int,
-  show_skolems: bool,
-  show_datatypes: bool,
-  show_consts: bool,
-  evals: term list,
-  formats: (term option * int list) list,
-  max_potential: int,
-  max_genuine: int,
-  check_potential: bool,
-  check_genuine: bool,
-  batch_size: int,
-  expect: string}
+type params =
+  {cards_assigns: (typ option * int list) list,
+   maxes_assigns: (styp option * int list) list,
+   iters_assigns: (styp option * int list) list,
+   bitss: int list,
+   bisim_depths: int list,
+   boxes: (typ option * bool option) list,
+   finitizes: (typ option * bool option) list,
+   monos: (typ option * bool option) list,
+   stds: (typ option * bool) list,
+   wfs: (styp option * bool option) list,
+   sat_solver: string,
+   blocking: bool,
+   falsify: bool,
+   debug: bool,
+   verbose: bool,
+   overlord: bool,
+   user_axioms: bool option,
+   assms: bool,
+   merge_type_vars: bool,
+   binary_ints: bool option,
+   destroy_constrs: bool,
+   specialize: bool,
+   star_linear_preds: bool,
+   fast_descrs: bool,
+   peephole_optim: bool,
+   timeout: Time.time option,
+   tac_timeout: Time.time option,
+   max_threads: int,
+   show_datatypes: bool,
+   show_consts: bool,
+   evals: term list,
+   formats: (term option * int list) list,
+   max_potential: int,
+   max_genuine: int,
+   check_potential: bool,
+   check_genuine: bool,
+   batch_size: int,
+   expect: string}
 
-type problem_extension = {
-  free_names: nut list,
-  sel_names: nut list,
-  nonsel_names: nut list,
-  rel_table: nut NameTable.table,
-  unsound: bool,
-  scope: scope}
-
+type problem_extension =
+  {free_names: nut list,
+   sel_names: nut list,
+   nonsel_names: nut list,
+   rel_table: nut NameTable.table,
+   unsound: bool,
+   scope: scope}
+ 
 type rich_problem = KK.problem * problem_extension
 
 fun pretties_for_formulas _ _ [] = []
@@ -191,10 +189,9 @@
          boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
          verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
          destroy_constrs, specialize, star_linear_preds, fast_descrs,
-         peephole_optim, tac_timeout, max_threads, show_skolems, show_datatypes,
-         show_consts, evals, formats, max_potential, max_genuine,
-         check_potential, check_genuine, batch_size, ...} =
-      params
+         peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
+         evals, formats, max_potential, max_genuine, check_potential,
+         check_genuine, batch_size, ...} = params
     val state_ref = Unsynchronized.ref state
     val pprint =
       if auto then
@@ -580,8 +577,7 @@
              : problem_extension) =
       let
         val (reconstructed_model, codatatypes_ok) =
-          reconstruct_hol_model {show_skolems = show_skolems,
-                                 show_datatypes = show_datatypes,
+          reconstruct_hol_model {show_datatypes = show_datatypes,
                                  show_consts = show_consts}
               scope formats frees free_names sel_names nonsel_names rel_table
               bounds
diff -r 8228b3a4a2ba -r eee4ee6a5cbe src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 25 00:25:44 2010 +0200
@@ -13,37 +13,37 @@
   type unrolled = styp * styp
   type wf_cache = (styp * (bool * bool)) list
 
-  type hol_context = {
-    thy: theory,
-    ctxt: Proof.context,
-    max_bisim_depth: int,
-    boxes: (typ option * bool option) list,
-    stds: (typ option * bool) list,
-    wfs: (styp option * bool option) list,
-    user_axioms: bool option,
-    debug: bool,
-    binary_ints: bool option,
-    destroy_constrs: bool,
-    specialize: bool,
-    star_linear_preds: bool,
-    fast_descrs: bool,
-    tac_timeout: Time.time option,
-    evals: term list,
-    case_names: (string * int) list,
-    def_table: const_table,
-    nondef_table: const_table,
-    user_nondefs: term list,
-    simp_table: const_table Unsynchronized.ref,
-    psimp_table: const_table,
-    choice_spec_table: const_table,
-    intro_table: const_table,
-    ground_thm_table: term list Inttab.table,
-    ersatz_table: (string * string) list,
-    skolems: (string * string list) list Unsynchronized.ref,
-    special_funs: special_fun list Unsynchronized.ref,
-    unrolled_preds: unrolled list Unsynchronized.ref,
-    wf_cache: wf_cache Unsynchronized.ref,
-    constr_cache: (typ * styp list) list Unsynchronized.ref}
+  type hol_context =
+    {thy: theory,
+     ctxt: Proof.context,
+     max_bisim_depth: int,
+     boxes: (typ option * bool option) list,
+     stds: (typ option * bool) list,
+     wfs: (styp option * bool option) list,
+     user_axioms: bool option,
+     debug: bool,
+     binary_ints: bool option,
+     destroy_constrs: bool,
+     specialize: bool,
+     star_linear_preds: bool,
+     fast_descrs: bool,
+     tac_timeout: Time.time option,
+     evals: term list,
+     case_names: (string * int) list,
+     def_table: const_table,
+     nondef_table: const_table,
+     user_nondefs: term list,
+     simp_table: const_table Unsynchronized.ref,
+     psimp_table: const_table,
+     choice_spec_table: const_table,
+     intro_table: const_table,
+     ground_thm_table: term list Inttab.table,
+     ersatz_table: (string * string) list,
+     skolems: (string * string list) list Unsynchronized.ref,
+     special_funs: special_fun list Unsynchronized.ref,
+     unrolled_preds: unrolled list Unsynchronized.ref,
+     wf_cache: wf_cache Unsynchronized.ref,
+     constr_cache: (typ * styp list) list Unsynchronized.ref}
 
   datatype fixpoint_kind = Lfp | Gfp | NoFp
   datatype boxability =
@@ -222,37 +222,37 @@
 type unrolled = styp * styp
 type wf_cache = (styp * (bool * bool)) list
 
-type hol_context = {
-  thy: theory,
-  ctxt: Proof.context,
-  max_bisim_depth: int,
-  boxes: (typ option * bool option) list,
-  stds: (typ option * bool) list,
-  wfs: (styp option * bool option) list,
-  user_axioms: bool option,
-  debug: bool,
-  binary_ints: bool option,
-  destroy_constrs: bool,
-  specialize: bool,
-  star_linear_preds: bool,
-  fast_descrs: bool,
-  tac_timeout: Time.time option,
-  evals: term list,
-  case_names: (string * int) list,
-  def_table: const_table,
-  nondef_table: const_table,
-  user_nondefs: term list,
-  simp_table: const_table Unsynchronized.ref,
-  psimp_table: const_table,
-  choice_spec_table: const_table,
-  intro_table: const_table,
-  ground_thm_table: term list Inttab.table,
-  ersatz_table: (string * string) list,
-  skolems: (string * string list) list Unsynchronized.ref,
-  special_funs: special_fun list Unsynchronized.ref,
-  unrolled_preds: unrolled list Unsynchronized.ref,
-  wf_cache: wf_cache Unsynchronized.ref,
-  constr_cache: (typ * styp list) list Unsynchronized.ref}
+type hol_context =
+  {thy: theory,
+   ctxt: Proof.context,
+   max_bisim_depth: int,
+   boxes: (typ option * bool option) list,
+   stds: (typ option * bool) list,
+   wfs: (styp option * bool option) list,
+   user_axioms: bool option,
+   debug: bool,
+   binary_ints: bool option,
+   destroy_constrs: bool,
+   specialize: bool,
+   star_linear_preds: bool,
+   fast_descrs: bool,
+   tac_timeout: Time.time option,
+   evals: term list,
+   case_names: (string * int) list,
+   def_table: const_table,
+   nondef_table: const_table,
+   user_nondefs: term list,
+   simp_table: const_table Unsynchronized.ref,
+   psimp_table: const_table,
+   choice_spec_table: const_table,
+   intro_table: const_table,
+   ground_thm_table: term list Inttab.table,
+   ersatz_table: (string * string) list,
+   skolems: (string * string list) list Unsynchronized.ref,
+   special_funs: special_fun list Unsynchronized.ref,
+   unrolled_preds: unrolled list Unsynchronized.ref,
+   wf_cache: wf_cache Unsynchronized.ref,
+   constr_cache: (typ * styp list) list Unsynchronized.ref}
 
 datatype fixpoint_kind = Lfp | Gfp | NoFp
 datatype boxability =
diff -r 8228b3a4a2ba -r eee4ee6a5cbe src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Apr 25 00:25:44 2010 +0200
@@ -65,7 +65,6 @@
    ("verbose", "false"),
    ("overlord", "false"),
    ("show_all", "false"),
-   ("show_skolems", "true"),
    ("show_datatypes", "false"),
    ("show_consts", "false"),
    ("format", "1"),
@@ -95,7 +94,6 @@
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
    ("dont_show_all", "show_all"),
-   ("hide_skolems", "show_skolems"),
    ("hide_datatypes", "show_datatypes"),
    ("hide_consts", "show_consts"),
    ("trust_potential", "check_potential"),
@@ -255,7 +253,6 @@
     val tac_timeout = lookup_time "tac_timeout"
     val max_threads = Int.max (0, lookup_int "max_threads")
     val show_all = debug orelse lookup_bool "show_all"
-    val show_skolems = show_all orelse lookup_bool "show_skolems"
     val show_datatypes = show_all orelse lookup_bool "show_datatypes"
     val show_consts = show_all orelse lookup_bool "show_consts"
     val formats = lookup_ints_assigns read_term_polymorphic "format" 0
@@ -265,9 +262,10 @@
     val max_genuine = Int.max (0, lookup_int "max_genuine")
     val check_potential = lookup_bool "check_potential"
     val check_genuine = lookup_bool "check_genuine"
-    val batch_size = case lookup_int_option "batch_size" of
-                       SOME n => Int.max (1, n)
-                     | NONE => if debug then 1 else 64
+    val batch_size =
+      case lookup_int_option "batch_size" of
+        SOME n => Int.max (1, n)
+      | NONE => if debug then 1 else 64
     val expect = lookup_string "expect"
   in
     {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
@@ -281,11 +279,10 @@
      star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
      peephole_optim = peephole_optim, timeout = timeout,
      tac_timeout = tac_timeout, max_threads = max_threads,
-     show_skolems = show_skolems, show_datatypes = show_datatypes,
-     show_consts = show_consts, formats = formats, evals = evals,
-     max_potential = max_potential, max_genuine = max_genuine,
-     check_potential = check_potential, check_genuine = check_genuine,
-     batch_size = batch_size, expect = expect}
+     show_datatypes = show_datatypes, show_consts = show_consts,
+     formats = formats, evals = evals, max_potential = max_potential,
+     max_genuine = max_genuine, check_potential = check_potential,
+     check_genuine = check_genuine, batch_size = batch_size, expect = expect}
   end
 
 fun default_params thy =
@@ -382,7 +379,7 @@
 val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
 
 val _ = OuterSyntax.improper_command "nitpick"
-            "try to find a counterexample for a given subgoal using Kodkod"
+            "try to find a counterexample for a given subgoal using Nitpick"
             K.diag parse_nitpick_command
 val _ = OuterSyntax.command "nitpick_params"
             "set and display the default parameters for Nitpick"
diff -r 8228b3a4a2ba -r eee4ee6a5cbe src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 25 00:25:44 2010 +0200
@@ -12,10 +12,10 @@
   type rep = Nitpick_Rep.rep
   type nut = Nitpick_Nut.nut
 
-  type params = {
-    show_skolems: bool,
-    show_datatypes: bool,
-    show_consts: bool}
+  type params =
+    {show_datatypes: bool,
+     show_consts: bool}
+
   type term_postprocessor =
     Proof.context -> string -> (typ -> term list) -> typ -> term -> term
 
@@ -51,10 +51,9 @@
 
 structure KK = Kodkod
 
-type params = {
-  show_skolems: bool,
-  show_datatypes: bool,
-  show_consts: bool}
+type params =
+  {show_datatypes: bool,
+   show_consts: bool}
 
 type term_postprocessor =
   Proof.context -> string -> (typ -> term list) -> typ -> term -> term
@@ -840,7 +839,7 @@
         t1 = t2
     end
 
-fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
+fun reconstruct_hol_model {show_datatypes, show_consts}
         ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
                       debug, binary_ints, destroy_constrs, specialize,
                       star_linear_preds, fast_descrs, tac_timeout, evals,
@@ -980,7 +979,7 @@
               | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
                                  [Const x])) all_frees
     val chunks = block_of_names true "Free variable" free_names @
-                 block_of_names show_skolems "Skolem constant" skolem_names @
+                 block_of_names true "Skolem constant" skolem_names @
                  block_of_names true "Evaluated term" eval_names @
                  block_of_datatypes @ block_of_codatatypes @
                  block_of_names show_consts "Constant"
diff -r 8228b3a4a2ba -r eee4ee6a5cbe src/HOL/Tools/Nitpick/nitpick_peephole.ML
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Sun Apr 25 00:25:44 2010 +0200
@@ -14,11 +14,11 @@
   type decl = Kodkod.decl
   type expr_assign = Kodkod.expr_assign
 
-  type name_pool = {
-    rels: n_ary_index list,
-    vars: n_ary_index list,
-    formula_reg: int,
-    rel_reg: int}
+  type name_pool =
+    {rels: n_ary_index list,
+     vars: n_ary_index list,
+     formula_reg: int,
+     rel_reg: int}
 
   val initial_pool : name_pool
   val not3_rel : n_ary_index
@@ -51,39 +51,38 @@
   val num_seq : int -> int -> int_expr list
   val s_and : formula -> formula -> formula
 
-  type kodkod_constrs = {
-    kk_all: decl list -> formula -> formula,
-    kk_exist: decl list -> formula -> formula,
-    kk_formula_let: expr_assign list -> formula -> formula,
-    kk_formula_if: formula -> formula -> formula -> formula,
-    kk_or: formula -> formula -> formula,
-    kk_not: formula -> formula,
-    kk_iff: formula -> formula -> formula,
-    kk_implies: formula -> formula -> formula,
-    kk_and: formula -> formula -> formula,
-    kk_subset: rel_expr -> rel_expr -> formula,
-    kk_rel_eq: rel_expr -> rel_expr -> formula,
-    kk_no: rel_expr -> formula,
-    kk_lone: rel_expr -> formula,
-    kk_one: rel_expr -> formula,
-    kk_some: rel_expr -> formula,
-    kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
-    kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
-    kk_union: rel_expr -> rel_expr -> rel_expr,
-    kk_difference: rel_expr -> rel_expr -> rel_expr,
-    kk_override: rel_expr -> rel_expr -> rel_expr,
-    kk_intersect: rel_expr -> rel_expr -> rel_expr,
-    kk_product: rel_expr -> rel_expr -> rel_expr,
-    kk_join: rel_expr -> rel_expr -> rel_expr,
-    kk_closure: rel_expr -> rel_expr,
-    kk_reflexive_closure: rel_expr -> rel_expr,
-    kk_comprehension: decl list -> formula -> rel_expr,
-    kk_project: rel_expr -> int_expr list -> rel_expr,
-    kk_project_seq: rel_expr -> int -> int -> rel_expr,
-    kk_not3: rel_expr -> rel_expr,
-    kk_nat_less: rel_expr -> rel_expr -> rel_expr,
-    kk_int_less: rel_expr -> rel_expr -> rel_expr
-  }
+  type kodkod_constrs =
+    {kk_all: decl list -> formula -> formula,
+     kk_exist: decl list -> formula -> formula,
+     kk_formula_let: expr_assign list -> formula -> formula,
+     kk_formula_if: formula -> formula -> formula -> formula,
+     kk_or: formula -> formula -> formula,
+     kk_not: formula -> formula,
+     kk_iff: formula -> formula -> formula,
+     kk_implies: formula -> formula -> formula,
+     kk_and: formula -> formula -> formula,
+     kk_subset: rel_expr -> rel_expr -> formula,
+     kk_rel_eq: rel_expr -> rel_expr -> formula,
+     kk_no: rel_expr -> formula,
+     kk_lone: rel_expr -> formula,
+     kk_one: rel_expr -> formula,
+     kk_some: rel_expr -> formula,
+     kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
+     kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
+     kk_union: rel_expr -> rel_expr -> rel_expr,
+     kk_difference: rel_expr -> rel_expr -> rel_expr,
+     kk_override: rel_expr -> rel_expr -> rel_expr,
+     kk_intersect: rel_expr -> rel_expr -> rel_expr,
+     kk_product: rel_expr -> rel_expr -> rel_expr,
+     kk_join: rel_expr -> rel_expr -> rel_expr,
+     kk_closure: rel_expr -> rel_expr,
+     kk_reflexive_closure: rel_expr -> rel_expr,
+     kk_comprehension: decl list -> formula -> rel_expr,
+     kk_project: rel_expr -> int_expr list -> rel_expr,
+     kk_project_seq: rel_expr -> int -> int -> rel_expr,
+     kk_not3: rel_expr -> rel_expr,
+     kk_nat_less: rel_expr -> rel_expr -> rel_expr,
+     kk_int_less: rel_expr -> rel_expr -> rel_expr}
 
   val kodkod_constrs : bool -> int -> int -> int -> kodkod_constrs
 end;
@@ -94,11 +93,11 @@
 open Kodkod
 open Nitpick_Util
 
-type name_pool = {
-  rels: n_ary_index list,
-  vars: n_ary_index list,
-  formula_reg: int,
-  rel_reg: int}
+type name_pool =
+  {rels: n_ary_index list,
+   vars: n_ary_index list,
+   formula_reg: int,
+   rel_reg: int}
 
 (* If you add new built-in relations, make sure to increment the counters here
    as well to avoid name clashes (which fortunately would be detected by
@@ -204,39 +203,38 @@
   | s_and _ False = False
   | s_and f1 f2 = And (f1, f2)
 
-type kodkod_constrs = {
-  kk_all: decl list -> formula -> formula,
-  kk_exist: decl list -> formula -> formula,
-  kk_formula_let: expr_assign list -> formula -> formula,
-  kk_formula_if: formula -> formula -> formula -> formula,
-  kk_or: formula -> formula -> formula,
-  kk_not: formula -> formula,
-  kk_iff: formula -> formula -> formula,
-  kk_implies: formula -> formula -> formula,
-  kk_and: formula -> formula -> formula,
-  kk_subset: rel_expr -> rel_expr -> formula,
-  kk_rel_eq: rel_expr -> rel_expr -> formula,
-  kk_no: rel_expr -> formula,
-  kk_lone: rel_expr -> formula,
-  kk_one: rel_expr -> formula,
-  kk_some: rel_expr -> formula,
-  kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
-  kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
-  kk_union: rel_expr -> rel_expr -> rel_expr,
-  kk_difference: rel_expr -> rel_expr -> rel_expr,
-  kk_override: rel_expr -> rel_expr -> rel_expr,
-  kk_intersect: rel_expr -> rel_expr -> rel_expr,
-  kk_product: rel_expr -> rel_expr -> rel_expr,
-  kk_join: rel_expr -> rel_expr -> rel_expr,
-  kk_closure: rel_expr -> rel_expr,
-  kk_reflexive_closure: rel_expr -> rel_expr,
-  kk_comprehension: decl list -> formula -> rel_expr,
-  kk_project: rel_expr -> int_expr list -> rel_expr,
-  kk_project_seq: rel_expr -> int -> int -> rel_expr,
-  kk_not3: rel_expr -> rel_expr,
-  kk_nat_less: rel_expr -> rel_expr -> rel_expr,
-  kk_int_less: rel_expr -> rel_expr -> rel_expr
-}
+type kodkod_constrs =
+  {kk_all: decl list -> formula -> formula,
+   kk_exist: decl list -> formula -> formula,
+   kk_formula_let: expr_assign list -> formula -> formula,
+   kk_formula_if: formula -> formula -> formula -> formula,
+   kk_or: formula -> formula -> formula,
+   kk_not: formula -> formula,
+   kk_iff: formula -> formula -> formula,
+   kk_implies: formula -> formula -> formula,
+   kk_and: formula -> formula -> formula,
+   kk_subset: rel_expr -> rel_expr -> formula,
+   kk_rel_eq: rel_expr -> rel_expr -> formula,
+   kk_no: rel_expr -> formula,
+   kk_lone: rel_expr -> formula,
+   kk_one: rel_expr -> formula,
+   kk_some: rel_expr -> formula,
+   kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
+   kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
+   kk_union: rel_expr -> rel_expr -> rel_expr,
+   kk_difference: rel_expr -> rel_expr -> rel_expr,
+   kk_override: rel_expr -> rel_expr -> rel_expr,
+   kk_intersect: rel_expr -> rel_expr -> rel_expr,
+   kk_product: rel_expr -> rel_expr -> rel_expr,
+   kk_join: rel_expr -> rel_expr -> rel_expr,
+   kk_closure: rel_expr -> rel_expr,
+   kk_reflexive_closure: rel_expr -> rel_expr,
+   kk_comprehension: decl list -> formula -> rel_expr,
+   kk_project: rel_expr -> int_expr list -> rel_expr,
+   kk_project_seq: rel_expr -> int -> int -> rel_expr,
+   kk_not3: rel_expr -> rel_expr,
+   kk_nat_less: rel_expr -> rel_expr -> rel_expr,
+   kk_int_less: rel_expr -> rel_expr -> rel_expr}
 
 (* We assume throughout that Kodkod variables have a "one" constraint. This is
    always the case if Kodkod's skolemization is disabled. *)
diff -r 8228b3a4a2ba -r eee4ee6a5cbe src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sun Apr 25 00:25:44 2010 +0200
@@ -10,32 +10,32 @@
   type styp = Nitpick_Util.styp
   type hol_context = Nitpick_HOL.hol_context
 
-  type constr_spec = {
-    const: styp,
-    delta: int,
-    epsilon: int,
-    exclusive: bool,
-    explicit_max: int,
-    total: bool}
+  type constr_spec =
+    {const: styp,
+     delta: int,
+     epsilon: int,
+     exclusive: bool,
+     explicit_max: int,
+     total: bool}
 
-  type dtype_spec = {
-    typ: typ,
-    card: int,
-    co: bool,
-    standard: bool,
-    complete: bool * bool,
-    concrete: bool * bool,
-    deep: bool,
-    constrs: constr_spec list}
+  type dtype_spec =
+    {typ: typ,
+     card: int,
+     co: bool,
+     standard: bool,
+     complete: bool * bool,
+     concrete: bool * bool,
+     deep: bool,
+     constrs: constr_spec list}
 
-  type scope = {
-    hol_ctxt: hol_context,
-    binarize: bool,
-    card_assigns: (typ * int) list,
-    bits: int,
-    bisim_depth: int,
-    datatypes: dtype_spec list,
-    ofs: int Typtab.table}
+  type scope =
+    {hol_ctxt: hol_context,
+     binarize: bool,
+     card_assigns: (typ * int) list,
+     bits: int,
+     bisim_depth: int,
+     datatypes: dtype_spec list,
+     ofs: int Typtab.table}
 
   val datatype_spec : dtype_spec list -> typ -> dtype_spec option
   val constr_spec : dtype_spec list -> styp -> constr_spec
@@ -61,32 +61,32 @@
 open Nitpick_Util
 open Nitpick_HOL
 
-type constr_spec = {
-  const: styp,
-  delta: int,
-  epsilon: int,
-  exclusive: bool,
-  explicit_max: int,
-  total: bool}
+type constr_spec =
+  {const: styp,
+   delta: int,
+   epsilon: int,
+   exclusive: bool,
+   explicit_max: int,
+   total: bool}
 
-type dtype_spec = {
-  typ: typ,
-  card: int,
-  co: bool,
-  standard: bool,
-  complete: bool * bool,
-  concrete: bool * bool,
-  deep: bool,
-  constrs: constr_spec list}
+type dtype_spec =
+  {typ: typ,
+   card: int,
+   co: bool,
+   standard: bool,
+   complete: bool * bool,
+   concrete: bool * bool,
+   deep: bool,
+   constrs: constr_spec list}
 
-type scope = {
-  hol_ctxt: hol_context,
-  binarize: bool,
-  card_assigns: (typ * int) list,
-  bits: int,
-  bisim_depth: int,
-  datatypes: dtype_spec list,
-  ofs: int Typtab.table}
+type scope =
+  {hol_ctxt: hol_context,
+   binarize: bool,
+   card_assigns: (typ * int) list,
+   bits: int,
+   bisim_depth: int,
+   datatypes: dtype_spec list,
+   ofs: int Typtab.table}
 
 datatype row_kind = Card of typ | Max of styp