# HG changeset patch
# User wenzelm
# Date 1191618257 -7200
# Node ID 62c48c4bee4873e1423d78f6a5a74fa12e6b5a81
# Parent  f33ff5fc1f7e4b48fbe4ce4da00bb269059b0abf
(co)induct: polymorhic taking'';

diff -r f33ff5fc1f7e -r 62c48c4bee48 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Oct 05 23:04:16 2007 +0200
+++ b/src/Tools/induct.ML	Fri Oct 05 23:04:17 2007 +0200
@@ -283,7 +283,7 @@
             val {T = xT, thy, ...} = Thm.rep_cterm cx;
             val ct = cert (tune t);
           in
-            if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
+            if Type.could_unify (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
             else error (Pretty.string_of (Pretty.block
              [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
               Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
@@ -615,7 +615,7 @@
           THEN' inner_atomize_tac) j))
         THEN' atomize_tac) i st |> Seq.maps (fn st' =>
             guess_instance (internalize more_consumes rule) i st'
-            |> Seq.map (rule_instance thy taking)
+            |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
             |> Seq.maps (fn rule' =>
               CASES (rule_cases rule' cases)
                 (Tactic.rtac rule' i THEN
@@ -672,7 +672,7 @@
       |> Seq.maps (RuleCases.consume [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
         guess_instance rule i st
-        |> Seq.map (rule_instance thy taking)
+        |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
         |> Seq.maps (fn rule' =>
           CASES (make_cases is_open rule' cases)
             (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))