--- a/src/HOL/Decision_Procs/MIR.thy Thu Mar 03 15:18:05 2011 +0100 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Mar 03 15:19:20 2011 +0100 @@ -5621,6 +5621,4 @@ apply mir done -unused_thms - end