src/Pure/search.ML
changeset 22360 26ead7ed4f4b
parent 22025 7c5896919eb8
child 23178 07ba6b58b3d2
     1.1 --- a/src/Pure/search.ML	Mon Feb 26 21:34:16 2007 +0100
     1.2 +++ b/src/Pure/search.ML	Mon Feb 26 23:18:24 2007 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  	  case Seq.pull q of
     1.5  	      NONE         => depth used qs
     1.6  	    | SOME(st,stq) => 
     1.7 -		if satp st andalso not (member eq_thm used st)
     1.8 +		if satp st andalso not (member Thm.eq_thm used st)
     1.9  		then SOME(st, Seq.make
    1.10  			         (fn()=> depth (st::used) (stq::qs)))
    1.11  		else depth used (tac st :: stq :: qs)
    1.12 @@ -211,7 +211,7 @@
    1.13  (*Check for and delete duplicate proof states*)
    1.14  fun deleteAllMin prf heap = 
    1.15        if ThmHeap.is_empty heap then heap
    1.16 -      else if eq_thm (prf, #2 (ThmHeap.min heap))
    1.17 +      else if Thm.eq_thm (prf, #2 (ThmHeap.min heap))
    1.18        then deleteAllMin prf (ThmHeap.delete_min heap)
    1.19        else heap;
    1.20  
    1.21 @@ -269,7 +269,7 @@
    1.22  fun insert_with_level (lnth: int*int*thm, []) = [lnth]
    1.23    | insert_with_level ((l,m,th), (l',n,th')::nths) = 
    1.24        if  n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
    1.25 -      else if  n=m andalso eq_thm(th,th')
    1.26 +      else if  n=m andalso Thm.eq_thm(th,th')
    1.27                then (l',n,th')::nths
    1.28                else (l,m,th)::(l',n,th')::nths;
    1.29