src/HOL/Finite.ML

--- a/src/HOL/Finite.ML	Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Finite.ML	Wed Oct 04 13:10:03 1995 +0100
@@ -33,13 +33,13 @@
 
 (** Simplification for Fin **)
 
-val Fin_ss = set_ss addsimps Fin.intrs;
+Addsimps Fin.intrs;
 
 (*The union of two finite sets is finite*)
 val major::prems = goal Finite.thy
     "[| F: Fin(A);  G: Fin(A) |] ==> F Un G : Fin(A)";
 by (rtac (major RS Fin_induct) 1);
-by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_insert_left]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
 qed "Fin_UnI";
 
 (*Every subset of a finite set is finite*)
@@ -48,18 +48,19 @@
 	    rtac mp, etac spec,
 	    rtac subs]);
 by (rtac (fin RS Fin_induct) 1);
-by (simp_tac (Fin_ss addsimps [subset_Un_eq]) 1);
+by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
 by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
 by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
-by (ALLGOALS (asm_simp_tac Fin_ss));
+by (ALLGOALS Asm_simp_tac);
 qed "Fin_subset";
 
 (*The image of a finite set is finite*)
 val major::_ = goal Finite.thy
     "F: Fin(A) ==> h``F : Fin(h``A)";
 by (rtac (major RS Fin_induct) 1);
-by (simp_tac Fin_ss 1);
-by (asm_simp_tac (set_ss addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
+by (Simp_tac 1);
+by (asm_simp_tac
+    (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
 qed "Fin_imageI";
 
 val major::prems = goal Finite.thy 
@@ -70,7 +71,7 @@
 by (rtac (major RS Fin_induct) 1);
 by (rtac (Diff_insert RS ssubst) 2);
 by (ALLGOALS (asm_simp_tac
-                (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset]))));
+                (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
 qed "Fin_empty_induct_lemma";
 
 val prems = goal Finite.thy