1.1 --- a/src/HOL/Datatype_Universe.ML	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/Datatype_Universe.ML	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4  
     1.5  (** Scons vs Atom **)
     1.6  
     1.7 -Goalw [Atom_def,Scons_def,Push_Node_def,One_def]
     1.8 +Goalw [Atom_def,Scons_def,Push_Node_def,One_nat_def]
     1.9   "Scons M N ~= Atom(a)";
    1.10  by (rtac notI 1);
    1.11  by (etac (equalityD2 RS subsetD RS UnE) 1);
    1.12 @@ -141,11 +141,11 @@
    1.13  
    1.14  (** Injectiveness of Scons **)
    1.15  
    1.16 -Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> M<=M'";
    1.17 +Goalw [Scons_def,One_nat_def] "Scons M N <= Scons M' N' ==> M<=M'";
    1.18  by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
    1.19  qed "Scons_inject_lemma1";
    1.20  
    1.21 -Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> N<=N'";
    1.22 +Goalw [Scons_def,One_nat_def] "Scons M N <= Scons M' N' ==> N<=N'";
    1.23  by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
    1.24  qed "Scons_inject_lemma2";
    1.25  
    1.26 @@ -252,7 +252,7 @@
    1.27  by (rtac ntrunc_Atom 1);
    1.28  qed "ntrunc_Numb";
    1.29  
    1.30 -Goalw [Scons_def,ntrunc_def,One_def]
    1.31 +Goalw [Scons_def,ntrunc_def,One_nat_def]
    1.32      "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)";
    1.33  by (safe_tac (claset() addSIs [imageI]));
    1.34  by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
    1.35 @@ -266,7 +266,7 @@
    1.36  
    1.37  (** Injection nodes **)
    1.38  
    1.39 -Goalw [In0_def] "ntrunc 1' (In0 M) = {}";
    1.40 +Goalw [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
    1.41  by (Simp_tac 1);
    1.42  by (rewtac Scons_def);
    1.43  by (Blast_tac 1);
    1.44 @@ -277,7 +277,7 @@
    1.45  by (Simp_tac 1);
    1.46  qed "ntrunc_In0";
    1.47  
    1.48 -Goalw [In1_def] "ntrunc 1' (In1 M) = {}";
    1.49 +Goalw [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
    1.50  by (Simp_tac 1);
    1.51  by (rewtac Scons_def);
    1.52  by (Blast_tac 1);
    1.53 @@ -339,7 +339,7 @@
    1.54  
    1.55  (** Injection **)
    1.56  
    1.57 -Goalw [In0_def,In1_def,One_def] "In0(M) ~= In1(N)";
    1.58 +Goalw [In0_def,In1_def,One_nat_def] "In0(M) ~= In1(N)";
    1.59  by (rtac notI 1);
    1.60  by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
    1.61  qed "In0_not_In1";