# HG changeset patch
# User wenzelm
# Date 1163362491 -3600
# Node ID 6d709b9bea1a46f7c4a30318769c47110ac82f96
# Parent  26fc3a45547c168f27354949db22166446b5b49d
removed dead code;

diff -r 26fc3a45547c -r 6d709b9bea1a 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
diff -r 26fc3a45547c -r 6d709b9bea1a src/Pure/Isar/outer_parse.ML
--- 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 *)