--- a/src/Tools/induct.ML Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Tools/induct.ML Sat Nov 08 21:31:51 2014 +0100
@@ -602,7 +602,8 @@
val rule' = Thm.incr_indexes (maxidx + 1) rule;
val concl = Logic.strip_assums_concl goal;
in
- Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
+ Unify.smash_unifiers (Context.Proof ctxt)
+ [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
|> Seq.map (fn env => Drule.instantiate_normalize (dest_env thy env) rule')
end
end