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/Import/shuffler.ML
changeset 39159 0dec18004e75
parent 38864 4abe644fcea5
child 39557 fe5722fce758 
--- a/src/HOL/Import/shuffler.ML	Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Import/shuffler.ML	Mon Sep 06 19:13:10 2010 +0200
@@ -346,7 +346,7 @@
 fun beta_fun thy assume t =
     SOME (Thm.beta_conversion true (cterm_of thy t))
 
-val meta_sym_rew = thm "refl"
+val meta_sym_rew = @{thm refl}
 
 fun equals_fun thy assume t =
     case t of
isabelle