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/Prolog/HOHH.ML
changeset 17892 62c397c17d18
parent 17311 5b1d47d920ce 
--- a/src/HOL/Prolog/HOHH.ML	Tue Oct 18 17:59:24 2005 +0200
+++ b/src/HOL/Prolog/HOHH.ML	Tue Oct 18 17:59:25 2005 +0200
@@ -54,7 +54,10 @@
     | _                             => [thm]
 in map zero_var_indexes (at thm) end;
 
-val atomize_ss = empty_ss setmksimps (mksimps mksimps_pairs) addsimps [
+val atomize_ss =
+  Simplifier.theory_context (the_context ()) empty_ss
+  setmksimps (mksimps mksimps_pairs)
+  addsimps [
         all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
         imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
         imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
isabelle