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/Pure/meta_simplifier.ML
changeset 28620 9846d772b306
parent 27865 27a8ad9612a3
child 28839 32d498cf7595 
--- a/src/Pure/meta_simplifier.ML	Thu Oct 16 22:44:28 2008 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Oct 16 22:44:29 2008 +0200
@@ -1344,7 +1344,7 @@
   |> Thm.adjust_maxidx_thm ~1
   |> Drule.gen_all;
 
-val hhf_ss = empty_ss addsimps [Drule.norm_hhf_eq];
+val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs;
 
 in
isabelle