diff -r 480303e3fa08 -r c1e3e7d3f469 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Wed Dec 05 03:12:52 2001 +0100
+++ b/src/Provers/hypsubst.ML	Wed Dec 05 03:13:21 2001 +0100
@@ -261,22 +261,11 @@
   Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac));
 
 
-(* attributes *)
-
-fun symmetric_rule thm =
-  thm RS Drule.symmetric_thm handle THM _ =>
-  thm RS Data.sym handle THM _ => error "Failed to apply symmetry of == or =";
-
-fun gen_symmetric x = Drule.rule_attribute (K symmetric_rule);
-
-
 (* theory setup *)
 
 val hypsubst_setup =
  [Method.add_methods
   [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
-   ("subst", subst_meth, "substitution")],
-  Attrib.add_attributes
-  [("symmetric", (gen_symmetric, gen_symmetric), "resolution with symmetry of == or =")]];
+   ("subst", subst_meth, "substitution")]];
 
 end;