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.
tuned
authorhaftmann
Wed, 22 Jan 2020 19:17:59 +0000
changeset 71403 43c2355648d2
parent 71402 fb9edfe035e1
child 71404 f2b783abfbe7
tuned
src/Pure/raw_simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/raw_simplifier.ML	Wed Jan 22 19:17:58 2020 +0000
+++ b/src/Pure/raw_simplifier.ML	Wed Jan 22 19:17:59 2020 +0000
@@ -357,9 +357,9 @@
 fun map_simpset1 f = map_simpset (fn Simpset (ss1, ss2) => Simpset (map_ss1 f ss1, ss2));
 fun map_simpset2 f = map_simpset (fn Simpset (ss1, ss2) => Simpset (ss1, map_ss2 f ss2));
 
-fun simpset_map ctxt f ss = ctxt |> map_simpset (K ss) |> f |> Context.Proof |> Simpset.get;
+fun put_simpset ss = map_simpset (K ss);
 
-fun put_simpset ss = map_simpset (K ss);
+fun simpset_map ctxt f ss = ctxt |> put_simpset ss |> f |> simpset_of;
 
 val empty_simpset = put_simpset empty_ss;
isabelle