1 files changed, 0 insertions, 16 deletions
diff --git a/spartan/lib/congruence.ML b/spartan/lib/congruence.ML
deleted file mode 100644
index bb7348c..0000000
--- a/spartan/lib/congruence.ML
+++ /dev/null
@@ -1,16 +0,0 @@
-signature Sym_Attr_Data =
-sig
-  val name: string
-  val symmetry_rule: thm
-end
-
-functor Sym_Attr (D: Sym_Attr_Data) =
-struct
-  local
-    val distinct_prems = the_single o Seq.list_of o Tactic.distinct_subgoals_tac
-  in
-    val attr = Thm.rule_attribute []
-      (K (fn th => distinct_prems (th RS D.symmetry_rule) handle THM _ => th))
-    val setup = Attrib.setup (Binding.name D.name) (Scan.succeed attr) ""
-  end
-end