--- 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) =