src/Provers/order.ML
changeset 19617 7cb4b67d4b97
parent 19250 932a50e2332f
child 22578 b0eb5652f210
--- a/src/Provers/order.ML	Thu May 11 19:15:16 2006 +0200
+++ b/src/Provers/order.ML	Thu May 11 19:19:31 2006 +0200
@@ -734,7 +734,7 @@
 in
   (* looking for x <= y: any path from x to y is sufficient *)
   case subgoal of (Le (x, y, _)) => (
-  if sccGraph = [] then raise Cannot else ( 
+  if null sccGraph then raise Cannot else ( 
    let 
     val xi = getIndex x ntc
     val yi = getIndex y ntc
@@ -758,7 +758,7 @@
  (* looking for x < y: particular path required, which is not necessarily
     found by normal dfs *)
  |   (Less (x, y, _)) => (
-  if sccGraph = [] then raise Cannot else (
+  if null sccGraph then raise Cannot else (
    let 
     val xi = getIndex x ntc
     val yi = getIndex y ntc
@@ -780,9 +780,9 @@
  )
 | (NotEq (x, y, _)) => (
   (* if there aren't any edges that are candidate for a ~= raise Cannot *)
-  if neqE = [] then raise Cannot
+  if null neqE then raise Cannot
   (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *)
-  else if sccSubgraphs = [] then (
+  else if null sccSubgraphs then (
      (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
        ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
           if  (x aconv x' andalso y aconv y') then p