src/Tools/eqsubst.ML
changeset 52223 5bb6ae8acb87
parent 51717 9e7d1c139569
child 52234 6ffcce211047
     1.1 --- a/src/Tools/eqsubst.ML	Wed May 29 16:12:05 2013 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Wed May 29 18:25:11 2013 +0200
     1.3 @@ -365,12 +365,6 @@
     1.4        (* ~j because new asm starts at back, thus we subtract 1 *)
     1.5        Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
     1.6        (Tactic.dtac preelimrule i th2)
     1.7 -
     1.8 -      (* (Thm.bicompose
     1.9 -                 false (* use unification *)
    1.10 -                 (true, (* elim resolution *)
    1.11 -                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
    1.12 -                 i th2) *)
    1.13      end;
    1.14  
    1.15