--- a/src/HOL/Tools/sat_funcs.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/sat_funcs.ML Tue Oct 27 17:34:00 2009 +0100
@@ -92,8 +92,8 @@
(* ------------------------------------------------------------------------- *)
datatype CLAUSE = NO_CLAUSE
- | ORIG_CLAUSE of Thm.thm
- | RAW_CLAUSE of Thm.thm * (int * Thm.cterm) list;
+ | ORIG_CLAUSE of thm
+ | RAW_CLAUSE of thm * (int * cterm) list;
(* ------------------------------------------------------------------------- *)
(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *)