# HG changeset patch
# User wenzelm
# Date 1139255940 -3600
# Node ID 057b32b8f1fd9c551bd39cbc35bc30a171dbc06f
# Parent  66ecb05f92c8cd754cd2adf7d4946a225fb3be1c
Logic.rlist_abs;

diff -r 66ecb05f92c8 -r 057b32b8f1fd src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Mon Feb 06 20:58:59 2006 +0100
+++ b/src/Provers/induct_method.ML	Mon Feb 06 20:59:00 2006 +0100
@@ -307,8 +307,8 @@
       |> `(Thm.prop_of #> Logic.strip_assums_concl)
       |-> (fn pred $ arg =>
         Drule.cterm_instantiate
-          [(cert (Term.head_of pred), cert (Unify.rlist_abs (xs, body))),
-           (cert (Term.head_of arg), cert (Unify.rlist_abs (xs, v)))]);
+          [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
+           (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
 
     fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
       | goal_concl 0 xs B =