diff -r 75ee8475c37e -r a5a09855e424 src/Tools/Argo/argo_thy.ML
--- 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) =