# HG changeset patch
# User krauss
# Date 1217867067 -7200
# Node ID 50a67d1977d7e95253966318a0b02093d1040108
# Parent  c8a462f1f4a2b3626da16a51b76127c956bcdc85
removed dead code

diff -r c8a462f1f4a2 -r 50a67d1977d7 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Aug 04 17:13:34 2008 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Aug 04 18:24:27 2008 +0200
@@ -123,38 +123,6 @@
            end
       end
 
-(* find all positions of elements in a list *)
-fun find_index_list P =
-    let fun find _ [] = []
-          | find n (x :: xs) = if P x then n :: find (n + 1) xs else find (n + 1) xs
-    in find 0 end
-
-(* simple breadth-first search algorithm for the table *)
-fun bfs_search_table nodes =
-    case nodes of
-      [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun search_table (breadth search finished)"
-    | (node::rnodes) => let
-        val (order, table) = node
-      in
-        case table of
-          [] => SOME (foldr (fn (c, order) => c :: transform_order c order) [] (rev order))
-        | _ => let
-            val cols = find_index_list (check_col) (transpose table)
-          in
-            case cols of
-              [] => NONE
-            | _ => let
-              val newtables = map (transform_table table) cols
-              val neworders = map (fn c => c :: order) cols
-              val newnodes = neworders ~~ newtables
-            in
-              bfs_search_table (rnodes @ newnodes)
-            end
-          end
-      end
-
-fun nsearch_table table = bfs_search_table [([], table)]
-
 (** Proof Reconstruction **)
 
 (* prove row :: cell list -> tactic *)