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/Hoare/hoare_tac.ML
changeset 81519 cdc43c0fdbfc
parent 80703 cc4ecaa8e96e
child 81522 e8b388c2b490 
--- a/src/HOL/Hoare/hoare_tac.ML	Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML	Sat Nov 30 22:33:21 2024 +0100
@@ -87,7 +87,7 @@
 
 fun Mset ctxt prop =
   let
-    val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())];
+    val [(Mset, _), (P, _)] = Variable.variant_names ctxt [("Mset", ()), ("P", ())];
 
     val vars = get_vars prop;
     val varsT = fastype_of (mk_bodyC vars);
isabelle