# HG changeset patch
# User berghofe
# Date 1035212259 -7200
# Node ID 58bb243dbafbffe769f6f1f931eacd5ff0a52407
# Parent  95b95cdb47047ab884b4d6e110bbce9c4a462b35
Changed type of Logic.strip_horn.

diff -r 95b95cdb4704 -r 58bb243dbafb src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Fri Oct 18 17:50:13 2002 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Mon Oct 21 16:57:39 2002 +0200
@@ -29,7 +29,7 @@
 
 fun prove_goal' sg p f =
   let
-    val (_, As, B) = Logic.strip_horn p;
+    val (As, B) = Logic.strip_horn p;
     val cAs = map (cterm_of sg) As;
     val asms = map (norm_hhf_rule o assume) cAs;
     fun check thm = if nprems_of thm > 0 then