src/HOL/Tools/datatype_realizer.ML
changeset 13656 58bb243dbafb
parent 13641 63d1790a43ed
child 13708 a3a410782c95
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Fri Oct 18 17:50:13 2002 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Mon Oct 21 16:57:39 2002 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  fun prove_goal' sg p f =
     1.6    let
     1.7 -    val (_, As, B) = Logic.strip_horn p;
     1.8 +    val (As, B) = Logic.strip_horn p;
     1.9      val cAs = map (cterm_of sg) As;
    1.10      val asms = map (norm_hhf_rule o assume) cAs;
    1.11      fun check thm = if nprems_of thm > 0 then