changeset 29805 | a5da150bd0ab |
parent 29650 | cc3958d31b1d |
child 29834 | 3237cfd177f3 |
--- a/src/HOL/Library/reflection.ML Thu Feb 05 11:45:15 2009 +0100 +++ b/src/HOL/Library/reflection.ML Thu Feb 05 11:49:15 2009 +0100 @@ -306,8 +306,8 @@ fun genreify_tac ctxt eqs to i = (fn st => let - val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1)) - val t = (case to of NONE => P | SOME x => x) + fun P () = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1)) + val t = (case to of NONE => P () | SOME x => x) val th = (genreif ctxt eqs t) RS ssubst in rtac th i st end);