# HG changeset patch
# User smolkas
# Date 1357156381 -3600
# Node ID adbbe04b7c752fa3b92ca99a7b8bc11a564a58f4
# Parent  e409d9f8ec750f96484e04606198dc454cebb2f2
removed old, unused code

diff -r e409d9f8ec75 -r adbbe04b7c75 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Jan 02 20:52:39 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Jan 02 20:53:01 2013 +0100
@@ -41,7 +41,6 @@
   val direct_graph : direct_sequent list -> direct_graph
   val redirect_graph : atom list -> atom list -> ref_graph -> direct_proof
   val succedent_of_cases : (clause * direct_inference list) list -> clause
-  val chain_direct_proof : direct_proof -> direct_proof
   val string_of_direct_proof : direct_proof -> string
 end;
 
@@ -186,19 +185,6 @@
         in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end
   in redirect [] axioms seqs end
 
-val chain_direct_proof =
-  let
-    fun chain_inf cl0 (seq as Have (cs, c)) =
-          seq
-      | chain_inf _ (Cases cases) = Cases (map chain_case cases)
-    and chain_case (c, is) = (c, chain_proof (SOME c) is)
-    and chain_proof _ [] = []
-      | chain_proof (SOME prev) (i :: is) =
-        chain_inf prev i :: chain_proof (SOME (succedent_of_inference i)) is
-      | chain_proof _ (i :: is) =
-        i :: chain_proof (SOME (succedent_of_inference i)) is
-  in chain_proof NONE end
-
 fun indent 0 = ""
   | indent n = "  " ^ indent (n - 1)