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