fixed typo
authorbulwahn
Mon, 25 Jul 2011 11:21:44 +0200
changeset 43959 285ffb18da30
parent 43958 bc5e767f0f46
child 43960 c2554cc82d34
fixed typo
src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Mon Jul 25 10:43:14 2011 +0200
+++ b/src/HOL/Library/reflection.ML	Mon Jul 25 11:21:44 2011 +0200
@@ -305,7 +305,7 @@
   in rtac th i end);
 
     (* Reflection calls reification and uses the correctness *)
-        (* theorem assumed to be the dead of the list *)
+        (* theorem assumed to be the head of the list *)
 fun gen_reflection_tac ctxt conv corr_thms raw_eqs to = SUBGOAL (fn (goal, i) =>
   let
     val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)