# HG changeset patch # User bulwahn # Date 1311585704 -7200 # Node ID 285ffb18da304977cdb0feaadff91083b1132b90 # Parent bc5e767f0f464f67bdeada2c527392256c4c631b fixed typo diff -r bc5e767f0f46 -r 285ffb18da30 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)