Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Logic.rlist_abs;
authorwenzelm
Mon, 06 Feb 2006 20:59:00 +0100
changeset 18933 057b32b8f1fd
parent 18932 66ecb05f92c8
child 18934 0342b7c21388
Logic.rlist_abs;
src/Provers/induct_method.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle