diff -r e15b74577368 -r a5da150bd0ab src/HOL/Library/reflection.ML
--- 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);