Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoiding warning for a duplicate rewrite rule in preprocessing of the predicate compiler
authorbulwahn
Tue, 31 Aug 2010 08:00:54 +0200
changeset 38952 694d0c88d86a
parent 38951 a16ee2b38db2
child 38953 0c38eb5fc4ca
avoiding warning for a duplicate rewrite rule in preprocessing of the predicate compiler
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Aug 31 08:00:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Aug 31 08:00:54 2010 +0200
@@ -259,7 +259,8 @@
 
 fun rewrite_intros thy =
   Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
-  #> Simplifier.full_simplify (HOL_basic_ss addsimps @{thms bool_simps} addsimps @{thms nnf_simps})
+  #> Simplifier.full_simplify
+    (HOL_basic_ss addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
   #> map_term thy (maps_premises (split_conjs thy))
 
 fun print_specs options thy msg ths =
isabelle