src/HOL/Sum.ML
changeset 4089 96fba19bcbe2
parent 3842 b55686a7b22c
child 4477 b3e5857d8d99
     1.1 --- a/src/HOL/Sum.ML	Mon Nov 03 12:12:10 1997 +0100
     1.2 +++ b/src/HOL/Sum.ML	Mon Nov 03 12:13:18 1997 +0100
     1.3 @@ -78,11 +78,11 @@
     1.4  val Inr_inject = inj_Inr RS injD;
     1.5  
     1.6  goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
     1.7 -by (blast_tac (!claset addSDs [Inl_inject]) 1);
     1.8 +by (blast_tac (claset() addSDs [Inl_inject]) 1);
     1.9  qed "Inl_eq";
    1.10  
    1.11  goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
    1.12 -by (blast_tac (!claset addSDs [Inr_inject]) 1);
    1.13 +by (blast_tac (claset() addSDs [Inr_inject]) 1);
    1.14  qed "Inr_eq";
    1.15  
    1.16  AddIffs [Inl_eq, Inr_eq];
    1.17 @@ -119,11 +119,11 @@
    1.18  (** sum_case -- the selection operator for sums **)
    1.19  
    1.20  goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
    1.21 -by (blast_tac (!claset addIs [select_equality]) 1);
    1.22 +by (blast_tac (claset() addIs [select_equality]) 1);
    1.23  qed "sum_case_Inl";
    1.24  
    1.25  goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
    1.26 -by (blast_tac (!claset addIs [select_equality]) 1);
    1.27 +by (blast_tac (claset() addIs [select_equality]) 1);
    1.28  qed "sum_case_Inr";
    1.29  
    1.30  Addsimps [sum_case_Inl, sum_case_Inr];