# HG changeset patch
# User wenzelm
# Date 1273244586 -7200
# Node ID 08cd7eccb043754ca6754826fd0a39ffd02ec566
# Parent  bca8762be737e28a190c067ea5834dbcadfd4a13
use existing undefined function;

diff -r bca8762be737 -r 08cd7eccb043 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- 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), 
diff -r bca8762be737 -r 08cd7eccb043 src/HOL/Tools/Qelim/ferrante_rackoff_data.ML
--- 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)));