src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 41993 bd6296de1432
parent 41875 e3cd0dce9b1a
child 42361 23f352990944
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 17 14:43:53 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 17 22:07:17 2011 +0100
     1.3 @@ -14,6 +14,7 @@
     1.4  
     1.5    type params =
     1.6      {show_datatypes: bool,
     1.7 +     show_skolems: bool,
     1.8       show_consts: bool}
     1.9  
    1.10    type term_postprocessor =
    1.11 @@ -58,6 +59,7 @@
    1.12  
    1.13  type params =
    1.14    {show_datatypes: bool,
    1.15 +   show_skolems: bool,
    1.16     show_consts: bool}
    1.17  
    1.18  type term_postprocessor =
    1.19 @@ -859,7 +861,7 @@
    1.20          t1 = t2
    1.21      end
    1.22  
    1.23 -fun reconstruct_hol_model {show_datatypes, show_consts}
    1.24 +fun reconstruct_hol_model {show_datatypes, show_skolems, show_consts}
    1.25          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
    1.26                        debug, whacks, binary_ints, destroy_constrs, specialize,
    1.27                        star_linear_preds, total_consts, needs, tac_timeout,
    1.28 @@ -991,7 +993,7 @@
    1.29        ||> append (map_filter (free_name_for_term false) pseudo_frees)
    1.30      val real_free_names = map_filter (free_name_for_term true) real_frees
    1.31      val chunks = block_of_names true "Free variable" real_free_names @
    1.32 -                 block_of_names true "Skolem constant" skolem_names @
    1.33 +                 block_of_names show_skolems "Skolem constant" skolem_names @
    1.34                   block_of_names true "Evaluated term" eval_names @
    1.35                   block_of_datatypes @ block_of_codatatypes @
    1.36                   block_of_names show_consts "Constant"