--- 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
--- a/src/Pure/Isar/outer_parse.ML Sun Nov 12 21:14:49 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML Sun Nov 12 21:14:51 2006 +0100
@@ -222,10 +222,7 @@
val sort = group "sort" xname;
-fun gen_arity cod =
- Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- cod;
-
-val arity = gen_arity sort;
+val arity = Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort;
(* types *)