# HG changeset patch
# User berghofe
# Date 1035212878 -7200
# Node ID e36798726ca4b11a4951be999c5ae5995cc63e8f
# Parent  3cf622f6b0b2cc08608476fb31bb2b0c21593575
Changed type of Logic.strip_horn.

diff -r 3cf622f6b0b2 -r e36798726ca4 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Mon Oct 21 17:07:27 2002 +0200
+++ b/src/Pure/goals.ML	Mon Oct 21 17:07:58 2002 +0200
@@ -746,7 +746,7 @@
 fun prepare_proof atomic rths chorn =
   let val {sign, t=horn,...} = rep_cterm chorn;
       val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
-      val (_,As,B) = Logic.strip_horn(horn);
+      val (As, B) = Logic.strip_horn horn;
       val atoms = atomic andalso
             forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
       val (As,B) = if atoms then ([],horn) else (As,B);