src/HOL/Tools/Groebner_Basis/misc.ML

tuned is_comb/is_binop -- avoid construction of cterms;
removed conjunction rules (cf. HOLogic.conj_XXX);

(*  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 $ _ $ _ => Thm.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;