removed dead code;
authorwenzelm
Sun Nov 12 21:14:51 2006 +0100 (2006-11-12)
changeset 213146d709b9bea1a
parent 21313 26fc3a45547c
child 21315 be2669fe8363
removed dead code;
src/HOL/Bali/Basis.thy
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/HOL/Bali/Basis.thy	Sun Nov 12 21:14:49 2006 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Sun Nov 12 21:14:51 2006 +0100
     1.3 @@ -185,12 +185,6 @@
     1.4  
     1.5  section "quantifiers"
     1.6  
     1.7 -(*###to be phased out *)
     1.8 -ML {* 
     1.9 -fun noAll_simpset () = simpset() setmksimps 
    1.10 -	mksimps (List.filter (fn (x,_) => x<>"All") mksimps_pairs)
    1.11 -*}
    1.12 -
    1.13  lemma All_Ex_refl_eq2 [simp]: 
    1.14   "(!x. (? b. x = f b & Q b) \<longrightarrow> P x) = (!b. Q b --> P (f b))"
    1.15  apply auto
     2.1 --- a/src/Pure/Isar/outer_parse.ML	Sun Nov 12 21:14:49 2006 +0100
     2.2 +++ b/src/Pure/Isar/outer_parse.ML	Sun Nov 12 21:14:51 2006 +0100
     2.3 @@ -222,10 +222,7 @@
     2.4  
     2.5  val sort = group "sort" xname;
     2.6  
     2.7 -fun gen_arity cod =
     2.8 -  Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- cod;
     2.9 -
    2.10 -val arity = gen_arity sort;
    2.11 +val arity = Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort;
    2.12  
    2.13  
    2.14  (* types *)