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/Sequents/Modal0.thy
changeset 74302 6bc96f31cafd
parent 69605 a96320074298 
--- a/src/Sequents/Modal0.thy	Sun Sep 12 20:24:14 2021 +0200
+++ b/src/Sequents/Modal0.thy	Sun Sep 12 20:37:15 2021 +0200
@@ -20,8 +20,8 @@
   "_Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
 
 ML \<open>
-  fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
-  fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
+  fun star_tr c [s1, s2] = Syntax.const c $ seq_tr s1 $ seq_tr s2;
+  fun star_tr' c [s1, s2] = Syntax.const c $ seq_tr' s1 $ seq_tr' s2;
 \<close>
 
 parse_translation \<open>
isabelle