src/HOL/Induct/Multiset.ML
changeset 6024 cb87f103d114
parent 5983 79e301a6a51b
child 6162 484adda70b65
     1.1 --- a/src/HOL/Induct/Multiset.ML	Fri Dec 11 10:38:51 1998 +0100
     1.2 +++ b/src/HOL/Induct/Multiset.ML	Fri Dec 11 10:41:53 1998 +0100
     1.3 @@ -431,7 +431,7 @@
     1.4  by(blast_tac (claset() addDs [export lemma3]) 1);
     1.5  qed "all_accessible";
     1.6  
     1.7 -Close_locale();
     1.8 +Close_locale "MSOrd";
     1.9  
    1.10  Goal "wf(r) ==> wf(mult1 r)";
    1.11  by(blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);