--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Fri May 07 15:12:53 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Fri May 07 17:03:06 2010 +0200
@@ -258,8 +258,6 @@
val idealN = "ideal";
val fieldN = "field";
-fun undefined _ = raise Match;
-
val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm);
fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Fri May 07 15:12:53 2010 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Fri May 07 17:03:06 2010 +0200
@@ -52,8 +52,6 @@
val del = Thm.declaration_attribute (Data.map o del_data);
-fun undefined x = error "undefined";
-
fun add entry =
Thm.declaration_attribute (fn key => fn context => context |> Data.map
(del_data key #> cons (key, entry)));