src/Tools/eqsubst.ML

--- a/src/Tools/eqsubst.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Tools/eqsubst.ML	Wed May 29 18:25:11 2013 +0200
@@ -365,12 +365,6 @@
       (* ~j because new asm starts at back, thus we subtract 1 *)
       Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
       (Tactic.dtac preelimrule i th2)
-
-      (* (Thm.bicompose
-                 false (* use unification *)
-                 (true, (* elim resolution *)
-                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
-                 i th2) *)
     end;