# HG changeset patch
# User haftmann
# Date 1273070779 -7200
# Node ID 45f1a487cd278c93b894b2007fd2e719e10d5ef4
# Parent  db07d505e8136efa6a4b1cc1fcc5273980cae802
dropped unused file

diff -r db07d505e813 -r 45f1a487cd27 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Wed May 05 16:46:18 2010 +0200
+++ b/src/HOL/Groebner_Basis.thy	Wed May 05 16:46:19 2010 +0200
@@ -7,7 +7,6 @@
 theory Groebner_Basis
 imports Numeral_Simprocs
 uses
-  "Tools/Groebner_Basis/misc.ML"
   "Tools/Groebner_Basis/normalizer_data.ML"
   ("Tools/Groebner_Basis/normalizer.ML")
   ("Tools/Groebner_Basis/groebner.ML")
diff -r db07d505e813 -r 45f1a487cd27 src/HOL/Tools/Groebner_Basis/misc.ML
--- a/src/HOL/Tools/Groebner_Basis/misc.ML	Wed May 05 16:46:18 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(*  Title:      HOL/Tools/Groebner_Basis/misc.ML
-    ID:         $Id$
-    Author:     Amine Chaieb, TU Muenchen
-
-Very basic stuff for cterms.
-*)
-
-structure Misc =
-struct
-
-fun is_comb ct =
-  (case Thm.term_of ct of
-    _ $ _ => true
-  | _ => false);
-
-val concl = Thm.cprop_of #> Thm.dest_arg;
-
-fun is_binop ct ct' =
-  (case Thm.term_of ct' of
-    c $ _ $ _ => term_of ct aconv c
-  | _ => false);
-
-fun dest_binop ct ct' =
-  if is_binop ct ct' then Thm.dest_binop ct'
-  else raise CTERM ("dest_binop: bad binop", [ct, ct'])
-
-fun inst_thm inst = Thm.instantiate ([], inst);
-
-end;