Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/reflection.ML
changeset 35624 c4e29a0bb8c1
parent 32978 a473ba9a221d
child 36692 54b64d4ad524 
--- a/src/HOL/Library/reflection.ML	Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Library/reflection.ML	Sun Mar 07 11:57:16 2010 +0100
@@ -62,7 +62,7 @@
    fun tryext x = (x RS ext2 handle THM _ =>  x)
    val cong = (Goal.prove ctxt'' [] (map mk_def env)
                           (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
-                          (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x))
+                          (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x))
                                                         THEN rtac th' 1)) RS sym
 
    val (cong' :: vars') =
isabelle