src/HOL/Tools/Predicate_Compile/code_prolog.ML

     in
       list_comb (Const (c, Envir.subst_type subst cT),
         map (restore_term ctxt constant_table) (args ~~ argsT'))
     end
 
+    
+(* restore numerals in natural numbers *)
+
+fun restore_nat_numerals t =
+  if fastype_of t = @{typ nat} andalso is_some (try HOLogic.dest_nat t) then
+    HOLogic.mk_number @{typ nat} (HOLogic.dest_nat t)
+  else
+    (case t of
+        t1 $ t2 => restore_nat_numerals t1 $ restore_nat_numerals t2
+      | t => t)
+  
 (* values command *)
 
 val preprocess_options = Predicate_Compile_Aux.Options {
   expected_modes = NONE,
   proposed_modes = [],

                 (set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))  
             end
         end
   in
       foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
-        (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt' constant_table) (ts ~~ Ts))) tss) [])
+        (map (fn ts => HOLogic.mk_tuple 
+          (map (restore_nat_numerals o restore_term ctxt' constant_table) (ts ~~ Ts))) tss) [])
   end
 
 fun values_cmd print_modes soln raw_t state =
   let
     val ctxt = Toplevel.context_of state