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 signature;
authorwenzelm
Tue, 26 Dec 2023 20:11:25 +0100
changeset 79361 c28d4d1986f1
parent 79360 da22c8ab0112
child 79362 2187de552bd4
tuned signature;
src/Pure/zterm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/zterm.ML	Tue Dec 26 20:06:30 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 26 20:11:25 2023 +0100
@@ -198,7 +198,7 @@
     ZAxiom of string
   | ZOracle of string
   | ZBox of serial
-  | ZThm of {theory_name: string, thm_name: Thm_Name.T, pos: Position.T, serial: int};
+  | ZThm of {theory_name: string, thm_name: Thm_Name.T * Position.T, serial: int};
 
 datatype zproof =
     ZDummy                         (*dummy proof*)
@@ -817,10 +817,10 @@
 
 in
 
-fun thm_proof thy (name, pos) =
+fun thm_proof thy thm_name =
   let
     val thy_name = Context.theory_long_name thy;
-    fun zproof_name i = ZThm {theory_name = thy_name, thm_name = name, pos = pos, serial = i};
+    fun zproof_name i = ZThm {theory_name = thy_name, thm_name = thm_name, serial = i};
   in box_proof zproof_name thy end;
 
 fun add_box_proof thy hyps concl (zboxes, prf) =
isabelle