author | wenzelm |
Tue, 25 Mar 2008 21:01:01 +0100 | |
changeset 26395 | 9e0e4ce51313 |
parent 26394 | ddd7825ea4cd |
child 26396 | e44c5a1a47bd |
--- a/src/Pure/pure_thy.ML Tue Mar 25 21:01:00 2008 +0100 +++ b/src/Pure/pure_thy.ML Tue Mar 25 21:01:01 2008 +0100 @@ -195,7 +195,7 @@ val is_same = (case (new_res, old_res) of (NONE, NONE) => true - | (SOME (name1, ths1), SOME (name2, ths2)) => name1 = name2 andalso Thm.eq_thms (ths1, ths2) + | (SOME (_, ths1), SOME (_, ths2)) => Thm.eq_thms (ths1, ths2) | _ => false); val _ = if is_same orelse silent then ()