--- a/src/Tools/Argo/argo_thy.ML Fri Jan 20 17:22:54 2017 +0100
+++ b/src/Tools/Argo/argo_thy.ML Fri Jan 20 21:05:11 2017 +0100
@@ -19,9 +19,6 @@
type context
val context: context
- (* simplification *)
- val simplify: Argo_Rewr.context -> Argo_Rewr.context
-
(* enriching the context *)
val add_atom: Argo_Term.term -> context -> Argo_Lit.literal option * context
@@ -52,11 +49,6 @@
in (x, (cc, simplex)) end
-(* simplification *)
-
-val simplify = Argo_Cc.simplify #> Argo_Simplex.simplify
-
-
(* enriching the context *)
fun add_atom t (cc, simplex) =