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/ZF/Datatype.thy
changeset 80636 4041e7c8059d
parent 78800 0b3700d31758 
--- a/src/ZF/Datatype.thy	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/ZF/Datatype.thy	Sun Aug 04 17:39:47 2024 +0200
@@ -86,8 +86,8 @@
     val (lhs,rhs) = FOLogic.dest_eq old
     val (lhead, largs) = strip_comb lhs
     and (rhead, rargs) = strip_comb rhs
-    val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
-    val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
+    val lname = dest_Const_name lhead handle TERM _ => raise Match;
+    val rname = dest_Const_name rhead handle TERM _ => raise Match;
     val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname)
       handle Option.Option => raise Match;
     val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname)
isabelle