src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 60139 9fabfda0643f
parent 59970 e9f73d87d904
child 60193 9274808fa020
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 19 21:26:50 2015 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Apr 20 11:23:00 2015 +0200
     1.3 @@ -484,7 +484,6 @@
     1.4                            (uniterize_unarize_unbox_etc_type T1)
     1.5                            (uniterize_unarize_unbox_etc_type T2))
     1.6  
     1.7 -
     1.8      fun term_for_fun_or_set seen T T' j =
     1.9          let
    1.10            val k1 = card_of_type card_assigns (pseudo_domain_type T)
    1.11 @@ -880,6 +879,25 @@
    1.12          t1 = t2
    1.13      end
    1.14  
    1.15 +fun pretty_term_auto_global ctxt t =
    1.16 +  let
    1.17 +    fun add_fake_const s =
    1.18 +      Sign.declare_const_global ((Binding.name s, @{typ 'a}), NoSyn)
    1.19 +      #> #2
    1.20 +
    1.21 +    val globals = Term.add_const_names t []
    1.22 +      |> filter_out (String.isSubstring Long_Name.separator)
    1.23 +
    1.24 +    val fake_ctxt =
    1.25 +      ctxt |> Proof_Context.background_theory (fn thy =>
    1.26 +        thy
    1.27 +        |> Sign.map_naming (K Name_Space.global_naming)
    1.28 +        |> fold (perhaps o try o add_fake_const) globals
    1.29 +        |> Sign.restore_naming thy)
    1.30 +  in
    1.31 +    Syntax.pretty_term fake_ctxt t
    1.32 +  end
    1.33 +
    1.34  fun reconstruct_hol_model {show_types, show_skolems, show_consts}
    1.35          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
    1.36                        debug, whacks, binary_ints, destroy_constrs, specialize,
    1.37 @@ -893,8 +911,7 @@
    1.38          rel_table bounds =
    1.39    let
    1.40      val pool = Unsynchronized.ref []
    1.41 -    val (wacky_names as (_, base_step_names), ctxt) =
    1.42 -      add_wacky_syntax ctxt
    1.43 +    val (wacky_names as (_, base_step_names), ctxt) = add_wacky_syntax ctxt
    1.44      val hol_ctxt =
    1.45        {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
    1.46         wfs = wfs, user_axioms = user_axioms, debug = debug, whacks = whacks,
    1.47 @@ -948,8 +965,8 @@
    1.48                                     T T' (rep_of name)
    1.49        in
    1.50          Pretty.block (Pretty.breaks
    1.51 -            [Syntax.pretty_term ctxt t1, Pretty.str oper,
    1.52 -             Syntax.pretty_term ctxt t2])
    1.53 +            [pretty_term_auto_global ctxt t1, Pretty.str oper,
    1.54 +             pretty_term_auto_global ctxt t2])
    1.55        end
    1.56      fun pretty_for_data_type ({typ, card, complete, ...} : data_type_spec) =
    1.57        Pretty.block (Pretty.breaks
    1.58 @@ -960,7 +977,7 @@
    1.59              | _ => []) @
    1.60             [Pretty.str "=",
    1.61              Pretty.enum "," "{" "}"
    1.62 -                (map (Syntax.pretty_term ctxt) (all_values card typ) @
    1.63 +                (map (pretty_term_auto_global ctxt) (all_values card typ) @
    1.64                   (if fun_from_pair complete false then []
    1.65                    else [Pretty.str (unrep ())]))]))
    1.66      fun integer_data_type T =