1.1 --- a/src/HOL/Library/reflection.ML	Mon Jul 25 10:43:14 2011 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Mon Jul 25 11:21:44 2011 +0200
     1.3 @@ -305,7 +305,7 @@
     1.4    in rtac th i end);
     1.5  
     1.6      (* Reflection calls reification and uses the correctness *)
     1.7 -        (* theorem assumed to be the dead of the list *)
     1.8 +        (* theorem assumed to be the head of the list *)
     1.9  fun gen_reflection_tac ctxt conv corr_thms raw_eqs to = SUBGOAL (fn (goal, i) =>
    1.10    let
    1.11      val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)