1.1 --- a/src/HOL/Library/reflection.ML	Sat Mar 06 19:17:59 2010 +0000
     1.2 +++ b/src/HOL/Library/reflection.ML	Sun Mar 07 11:57:16 2010 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4     fun tryext x = (x RS ext2 handle THM _ =>  x)
     1.5     val cong = (Goal.prove ctxt'' [] (map mk_def env)
     1.6                            (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
     1.7 -                          (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x))
     1.8 +                          (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x))
     1.9                                                          THEN rtac th' 1)) RS sym
    1.10  
    1.11     val (cong' :: vars') =