1.1 --- a/src/HOL/Library/reflection.ML	Tue Nov 08 08:56:24 2011 +0100
     1.2 +++ b/src/HOL/Library/reflection.ML	Tue Nov 08 11:44:37 2011 +0100
     1.3 @@ -60,10 +60,11 @@
     1.4     fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t)))
     1.5       | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
     1.6     fun tryext x = (x RS ext2 handle THM _ =>  x)
     1.7 -   val cong = (Goal.prove ctxt'' [] (map mk_def env)
     1.8 -                          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
     1.9 -                          (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x))
    1.10 -                                                        THEN rtac th' 1)) RS sym
    1.11 +   val cong =
    1.12 +    (Goal.prove ctxt'' [] (map mk_def env)
    1.13 +      (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
    1.14 +      (fn {context, prems, ...} =>
    1.15 +        Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym
    1.16  
    1.17     val (cong' :: vars') =
    1.18         Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs)