# HG changeset patch
# User blanchet
# Date 1504821776 -7200
# Node ID ec8fceca7fb607c7e619e62c584ea144e9e1d7e2
# Parent  6950d3da13f8c490dbe1b993a4bbd4f8c09a3afc
nicer numeral output for nats and ints in Nunchaku

diff -r 6950d3da13f8 -r ec8fceca7fb6 src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML	Fri Sep 08 00:02:52 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML	Fri Sep 08 00:02:56 2017 +0200
@@ -224,8 +224,19 @@
           | _ => same ())
         end
       | term_of _ (NMatch _) = raise Fail "unexpected match";
+
+    fun rewrite_numbers (t as @{const Suc} $ _) =
+        (case try HOLogic.dest_nat t of
+          SOME n => HOLogic.mk_number @{typ nat} n
+        | NONE => t)
+      | rewrite_numbers (@{const Abs_Integ} $ (@{const Pair (nat, nat)} $ t $ u)) =
+        HOLogic.mk_number @{typ int} (HOLogic.dest_nat t - HOLogic.dest_nat u)
+      | rewrite_numbers (t $ u) = rewrite_numbers t $ rewrite_numbers u
+      | rewrite_numbers (Abs (s, T, t)) = Abs (s, T, rewrite_numbers t)
+      | rewrite_numbers t = t;
   in
     term_of []
+    #> rewrite_numbers
   end;
 
 fun isa_typ_entry_of_nun ctxt atomss (ty, atoms) =