src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 41993 bd6296de1432
parent 41875 e3cd0dce9b1a
child 42361 23f352990944
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 17 14:43:53 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 17 22:07:17 2011 +0100
@@ -14,6 +14,7 @@
 
   type params =
     {show_datatypes: bool,
+     show_skolems: bool,
      show_consts: bool}
 
   type term_postprocessor =
@@ -58,6 +59,7 @@
 
 type params =
   {show_datatypes: bool,
+   show_skolems: bool,
    show_consts: bool}
 
 type term_postprocessor =
@@ -859,7 +861,7 @@
         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,
@@ -991,7 +993,7 @@
       ||> 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"