# HG changeset patch
# User paulson
# Date 957446096 -7200
# Node ID c4aaa5936e0c2c07932442f93a20f4e5693d8e7f
# Parent  5bd6332640f82c522f938df131e69ec25f342bc4
Suc 0 -> 1

diff -r 5bd6332640f8 -r c4aaa5936e0c src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Thu May 04 15:14:44 2000 +0200
+++ b/src/HOL/Univ.ML	Thu May 04 15:14:56 2000 +0200
@@ -267,7 +267,7 @@
 
 (** Injection nodes **)
 
-Goalw [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
+Goalw [In0_def] "ntrunc 1 (In0 M) = {}";
 by (Simp_tac 1);
 by (rewtac Scons_def);
 by (Blast_tac 1);
@@ -278,7 +278,7 @@
 by (Simp_tac 1);
 qed "ntrunc_In0";
 
-Goalw [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
+Goalw [In1_def] "ntrunc 1 (In1 M) = {}";
 by (Simp_tac 1);
 by (rewtac Scons_def);
 by (Blast_tac 1);