# HG changeset patch
# User blanchet
# Date 1504821780 -7200
# Node ID 56456f3888674fc3117b0f862f09fa3951c07cd1
# Parent  ec8fceca7fb607c7e619e62c584ea144e9e1d7e2
eliminate artifact of translation in printed Nunchaku model

diff -r ec8fceca7fb6 -r 56456f388867 src/HOL/Tools/Nunchaku/nunchaku_collect.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Fri Sep 08 00:02:56 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Fri Sep 08 00:03:00 2017 +0200
@@ -792,7 +792,7 @@
 | Prim_Pattern of string
 | Any_Pattern;
 
-fun is_likely_pat_complete ctxt props =
+fun is_apparently_pat_complete ctxt props =
   let
     val is_Var_or_Bound = is_Var orf is_Bound;
 
@@ -965,7 +965,7 @@
                              (props,
                               [IRec (map2 (fn const => fn props =>
                                    {const = const, props = props,
-                                    pat_complete = is_likely_pat_complete ctxt props})
+                                    pat_complete = is_apparently_pat_complete ctxt props})
                                  consts propss)])
                            | NONE => def_or_spec ())
                          else if member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive]
diff -r ec8fceca7fb6 -r 56456f388867 src/HOL/Tools/Nunchaku/nunchaku_display.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_display.ML	Fri Sep 08 00:02:56 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_display.ML	Fri Sep 08 00:03:00 2017 +0200
@@ -32,6 +32,13 @@
   | sorting_str_of_term (Abs (_, T, t)) = "c" ^ sorting_str_of_typ T ^ " " ^ sorting_str_of_term t
   | sorting_str_of_term _ = "X";
 
+val basic_defs_sym = @{thms rmember_def[abs_def]};
+
+fun fold_basic_def ctxt =
+  let val thy = Proof_Context.theory_of ctxt in
+    Pattern.rewrite_term thy (map (Logic.dest_equals o Thm.prop_of) basic_defs_sym) []
+  end;
+
 fun pretty_of_isa_model_opt _ NONE =
     pretty_indent (Pretty.str "Model unavailable due to internal error")
   | pretty_of_isa_model_opt ctxt0 (SOME {type_model, free_model, pat_complete_model,
@@ -48,7 +55,10 @@
           val schematic_ctxt = ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic;
 
           val show_types = Config.get ctxt show_types;
-          val value' = value |> perhaps (try (Syntax.check_term schematic_ctxt));
+          val value' =
+            value
+            |> perhaps (try (Syntax.check_term schematic_ctxt))
+            |> perhaps (try (fold_basic_def ctxt));
           val T = fastype_of t;
           val T' = if T = dummyT then try fastype_of value' |> the_default T else T;
           val t' = t |> show_types ? Type.constraint T';