1.1 --- a/src/HOL/Groebner_Basis.thy	Wed May 05 16:46:18 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed May 05 16:46:19 2010 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  theory Groebner_Basis
     1.5  imports Numeral_Simprocs
     1.6  uses
     1.7 -  "Tools/Groebner_Basis/misc.ML"
     1.8    "Tools/Groebner_Basis/normalizer_data.ML"
     1.9    ("Tools/Groebner_Basis/normalizer.ML")
    1.10    ("Tools/Groebner_Basis/groebner.ML")

     2.1 --- a/src/HOL/Tools/Groebner_Basis/misc.ML	Wed May 05 16:46:18 2010 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,29 +0,0 @@
     2.4 -(*  Title:      HOL/Tools/Groebner_Basis/misc.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Amine Chaieb, TU Muenchen
     2.7 -
     2.8 -Very basic stuff for cterms.
     2.9 -*)
    2.10 -
    2.11 -structure Misc =
    2.12 -struct
    2.13 -
    2.14 -fun is_comb ct =
    2.15 -  (case Thm.term_of ct of
    2.16 -    _ $ _ => true
    2.17 -  | _ => false);
    2.18 -
    2.19 -val concl = Thm.cprop_of #> Thm.dest_arg;
    2.20 -
    2.21 -fun is_binop ct ct' =
    2.22 -  (case Thm.term_of ct' of
    2.23 -    c $ _ $ _ => term_of ct aconv c
    2.24 -  | _ => false);
    2.25 -
    2.26 -fun dest_binop ct ct' =
    2.27 -  if is_binop ct ct' then Thm.dest_binop ct'
    2.28 -  else raise CTERM ("dest_binop: bad binop", [ct, ct'])
    2.29 -
    2.30 -fun inst_thm inst = Thm.instantiate ([], inst);
    2.31 -
    2.32 -end;