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
Mon, 22 Jul 2019 11:40:04 +0200
changeset 70394 893d6373b484
parent 70393 9e53a98702b9
child 70395 af88c05696bd
tuned;
src/Pure/proofterm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/proofterm.ML	Mon Jul 22 11:39:30 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 22 11:40:04 2019 +0200
@@ -797,10 +797,10 @@
         val t = the_default Term.dummy opt;
         val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
       in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
-  | term_of Ts (Hyp t) = Hypt $ t
-  | term_of Ts (Oracle (_, t, _)) = Oraclet $ t
-  | term_of Ts MinProof = MinProoft
-  | term_of Ts (Promise (_, t, _)) = raise TERM ("Illegal proof promise", [t]);
+  | term_of _ (Hyp t) = Hypt $ t
+  | term_of _ (Oracle (_, t, _)) = Oraclet $ t
+  | term_of _ MinProof = MinProoft
+  | term_of _ (Promise (_, t, _)) = raise TERM ("Illegal proof promise", [t]);
 
 in
isabelle