changeset 21963 | 416a5338d2bb |
parent 21709 | 9cfd9eb9faec |
child 22095 | 07875394618e |
--- a/src/Provers/clasimp.ML Sat Dec 30 16:08:00 2006 +0100 +++ b/src/Provers/clasimp.ML Sat Dec 30 16:08:03 2006 +0100 @@ -125,7 +125,6 @@ fun addIff decls1 decls2 simp ((cs, ss), th) = let - val name = PureThy.get_name_hint th; val n = nprems_of th; val (elim, intro) = if n = 0 then decls1 else decls2; val zero_rotate = zero_var_indexes o rotate_prems n;