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/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
changeset 59058 a78612c67ec0
parent 58928 23d0ffd48006
child 61756 21c2b1f691d1 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -81,7 +81,7 @@
 val have_prefix = "f"
 
 fun label_ord ((s1, i1), (s2, i2)) =
-  (case int_ord (pairself String.size (s1, s2)) of
+  (case int_ord (apply2 String.size (s1, s2)) of
     EQUAL =>
     (case string_ord (s1, s2) of
       EQUAL => int_ord (i1, i2)
isabelle