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/Tools/Argo/argo_heap.ML
changeset 67560 0fa87bd86566
parent 63960 3daf02070be5 
--- a/src/Tools/Argo/argo_heap.ML	Thu Feb 01 13:55:10 2018 +0100
+++ b/src/Tools/Argo/argo_heap.ML	Thu Feb 01 15:12:57 2018 +0100
@@ -65,7 +65,7 @@
 
 fun weight_of vals t = fst (value_of vals t)
 
-fun less_than vals t1 t2 = weight_ord (weight_of vals t1, weight_of vals t2) = LESS
+fun less_than vals t1 t2 = is_less (weight_ord (weight_of vals t1, weight_of vals t2))
 
 fun rescale activity = activity div activity_rescale
 
@@ -163,7 +163,7 @@
 *)
 
 fun fix t (w, Some parent) (incr, vals) tree =
-      if weight_ord (weight_of vals parent, w) = LESS then
+      if is_less (weight_ord (weight_of vals parent, w)) then
         let val (tree1, tree2) = cut t (path_to vals parent []) tree
         in mk_heap' incr (merge tree1 tree2 (root t vals)) end
       else mk_heap incr vals tree
isabelle