src/HOL/Bali/Basis.thy

--- a/src/HOL/Bali/Basis.thy	Sun Nov 12 21:14:49 2006 +0100
+++ b/src/HOL/Bali/Basis.thy	Sun Nov 12 21:14:51 2006 +0100
@@ -185,12 +185,6 @@
 
 section "quantifiers"
 
-(*###to be phased out *)
-ML {* 
-fun noAll_simpset () = simpset() setmksimps 
-	mksimps (List.filter (fn (x,_) => x<>"All") mksimps_pairs)
-*}
-
 lemma All_Ex_refl_eq2 [simp]: 
  "(!x. (? b. x = f b & Q b) \<longrightarrow> P x) = (!b. Q b --> P (f b))"
 apply auto