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;
authorwenzelm
Wed, 06 Dec 2023 21:58:02 +0100
changeset 79160 b3a6a8ec27ef
parent 79159 05cdedece5a9
child 79161 3f532c76d0ad
tuned;
src/Pure/zterm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/zterm.ML	Wed Dec 06 21:28:40 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 21:58:02 2023 +0100
@@ -515,7 +515,7 @@
 
 fun equal_intr_proof thy t u prf1 prf2 =
   let
-    val {ztyp, zterm} = zterm_cache thy;
+    val {zterm, ...} = zterm_cache thy;
     val A = zterm t;
     val B = zterm u;
     val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom;
@@ -523,7 +523,7 @@
 
 fun equal_elim_proof thy t u prf1 prf2 =
   let
-    val {ztyp, zterm} = zterm_cache thy;
+    val {zterm, ...} = zterm_cache thy;
     val A = zterm t;
     val B = zterm u;
     val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom;
@@ -630,7 +630,7 @@
 
 fun permute_prems_proof thy prems' j k prf =
   let
-    val {ztyp, zterm} = zterm_cache thy;
+    val {zterm, ...} = zterm_cache thy;
     val n = length prems';
   in
     mk_ZAbsP (map zterm prems')
isabelle