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/Tools/SMT/z3_replay_methods.ML
changeset 63170 eae6549dbea2
parent 61841 4d3527b94f2a
child 65801 aeb776b5b054 
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Fri May 27 20:23:55 2016 +0200
@@ -616,7 +616,7 @@
 
 fun arith_th_lemma_tac ctxt prems =
   Method.insert_tac ctxt prems
-  THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms z3div_def z3mod_def})
+  THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms z3div_def z3mod_def})
   THEN' Arith_Data.arith_tac ctxt
 
 fun arith_th_lemma ctxt thms t =
isabelle