author | bulwahn |
Mon, 25 Jul 2011 11:21:44 +0200 | |
changeset 43959 | 285ffb18da30 |
parent 43958 | bc5e767f0f46 |
child 43960 | c2554cc82d34 |
--- 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)