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/S43.thy
changeset 74302 6bc96f31cafd
parent 69593 3dda49e08b9d
child 80914 d97fdabd9e2b 
--- a/src/Sequents/S43.thy	Sun Sep 12 20:24:14 2021 +0200
+++ b/src/Sequents/S43.thy	Sun Sep 12 20:37:15 2021 +0200
@@ -20,7 +20,7 @@
   let
     val tr  = seq_tr;
     fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
-      Const (\<^const_syntax>\<open>S43pi\<close>, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
+      Syntax.const \<^const_syntax>\<open>S43pi\<close> $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
   in [(\<^syntax_const>\<open>_S43pi\<close>, K s43pi_tr)] end
 \<close>
 
@@ -28,7 +28,7 @@
 let
   val tr' = seq_tr';
   fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
-    Const(\<^syntax_const>\<open>_S43pi\<close>, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
+    Syntax.const \<^syntax_const>\<open>_S43pi\<close> $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
 in [(\<^const_syntax>\<open>S43pi\<close>, K s43pi_tr')] end
 \<close>
isabelle