1.1 --- a/src/Pure/Isar/proof.ML	Fri Oct 02 20:51:32 2009 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Oct 02 21:39:06 2009 +0200
     1.3 @@ -431,9 +431,7 @@
     1.4  
     1.5  val refine = apply_text true;
     1.6  val refine_end = apply_text false;
     1.7 -
     1.8 -fun refine_insert [] = I
     1.9 -  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
    1.10 +fun refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
    1.11  
    1.12  end;
    1.13