src/Tools/Argo/argo_cc.ML

--- a/src/Tools/Argo/argo_cc.ML	Fri Jan 20 17:22:54 2017 +0100
+++ b/src/Tools/Argo/argo_cc.ML	Fri Jan 20 21:05:11 2017 +0100
@@ -33,9 +33,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
 
@@ -467,27 +464,6 @@
   end
 
 
-(* simplification *)
-
-(*
-  Only equalities are subject to normalizations. An equality between two expressions e1 and e2
-  is normalized, if e1 is less than e2 based on the expression ordering. If e1 and e2 are
-  syntactically equal, the equality between these two expressions is normalized to the true
-  expression.
-*)
-
-fun norm_eq env =
-  let val e1 = Argo_Rewr.get env 1 and e2 = Argo_Rewr.get env 2
-  in
-    (case Argo_Expr.expr_ord (e1, e2) of
-      EQUAL => SOME (Argo_Proof.Rewr_Eq_Refl, Argo_Rewr.E Argo_Expr.true_expr)
-    | LESS => NONE
-    | GREATER => SOME (Argo_Proof.Rewr_Eq_Symm, Argo_Rewr.E (Argo_Expr.mk_eq e2 e1)))
-  end
-
-val simplify = Argo_Rewr.func "(eq (? 1) (? 2))" norm_eq
-
-
 (* declaring atoms *)
 
 (*