src/HOL/Finite.ML
changeset 6024 cb87f103d114
parent 5782 7559f116cb10
child 6141 a6922171b396
     1.1 --- a/src/HOL/Finite.ML	Fri Dec 11 10:38:51 1998 +0100
     1.2 +++ b/src/HOL/Finite.ML	Fri Dec 11 10:41:53 1998 +0100
     1.3 @@ -675,7 +675,7 @@
     1.4  Delrules [empty_foldSetE];
     1.5  Delrules foldSet.intrs;
     1.6  
     1.7 -Close_locale();
     1.8 +Close_locale "LC";
     1.9  
    1.10  Open_locale "ACe"; 
    1.11  
    1.12 @@ -722,7 +722,7 @@
    1.13             [export fold_insert,insert_absorb, Int_insert_left]) 1);
    1.14  qed "fold_Un_disjoint2";
    1.15  
    1.16 -Close_locale();
    1.17 +Close_locale "ACe";
    1.18  
    1.19  Delrules ([empty_foldSetE] @ foldSet.intrs);
    1.20  Delsimps [foldSet_imp_finite];