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/HOLCF/Tools/Domain/domain_induction.ML
changeset 45654 cf10bde35973
parent 45133 2214ba5bdfff
child 51717 9e7d1c139569 
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -156,7 +156,7 @@
           fun con_thm p (con, args) =
             let
               val subgoal = con_assm false p (con, args)
-              val rules = prems @ con_rews @ simp_thms
+              val rules = prems @ con_rews @ @{thms simp_thms}
               val simplify = asm_simp_tac (HOL_basic_ss addsimps rules)
               fun arg_tac (lazy, _) =
                   rtac (if lazy then allI else case_UU_allI) 1
isabelle