src/HOL/Tools/Nitpick/nitpick_model.ML

   type rep = Nitpick_Rep.rep
   type nut = Nitpick_Nut.nut
 
   type params =
     {show_datatypes: bool,
+     show_skolems: bool,
      show_consts: bool}
 
   type term_postprocessor =
     Proof.context -> string -> (typ -> term list) -> typ -> term -> term
 

 
 structure KK = Kodkod
 
 type params =
   {show_datatypes: bool,
+   show_skolems: bool,
    show_consts: bool}
 
 type term_postprocessor =
   Proof.context -> string -> (typ -> term list) -> typ -> term -> term
 

         end
       else
         t1 = t2
     end
 
-fun reconstruct_hol_model {show_datatypes, show_consts}
+fun reconstruct_hol_model {show_datatypes, show_skolems, show_consts}
         ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
                       debug, whacks, binary_ints, destroy_constrs, specialize,
                       star_linear_preds, total_consts, needs, tac_timeout,
                       evals, case_names, def_tables, nondef_table, user_nondefs,
                       simp_table, psimp_table, choice_spec_table, intro_table,

                                      @{const_name bisim_iterator_max}]
                       o nickname_of)
       ||> append (map_filter (free_name_for_term false) pseudo_frees)
     val real_free_names = map_filter (free_name_for_term true) real_frees
     val chunks = block_of_names true "Free variable" real_free_names @
-                 block_of_names true "Skolem constant" skolem_names @
+                 block_of_names show_skolems "Skolem constant" skolem_names @
                  block_of_names true "Evaluated term" eval_names @
                  block_of_datatypes @ block_of_codatatypes @
                  block_of_names show_consts "Constant"
                                 noneval_nonskolem_nonsel_names
   in