--- a/src/Tools/induct.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Tools/induct.ML Tue Feb 10 14:48:26 2015 +0100
@@ -507,7 +507,7 @@
in
CASES (Rule_Cases.make_common (thy,
Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
- ((Method.insert_tac more_facts THEN' resolve_tac [rule'] THEN_ALL_NEW
+ ((Method.insert_tac more_facts THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
(if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
end)
end;
@@ -680,7 +680,7 @@
(case goal_concl n [] goal of
SOME concl =>
(compose_tac ctxt (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
- resolve_tac [asm_rl]) i
+ resolve_tac ctxt [asm_rl]) i
| NONE => all_tac)
end);
@@ -801,7 +801,7 @@
|> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
|> Seq.maps (fn rule' =>
CASES (rule_cases ctxt rule' cases)
- (resolve_tac [rule'] i THEN
+ (resolve_tac ctxt [rule'] i THEN
PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
end)
THEN_ALL_NEW_CASES
@@ -859,7 +859,7 @@
|> Seq.maps (fn rule' =>
CASES (Rule_Cases.make_common (thy,
Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
- (Method.insert_tac more_facts i THEN resolve_tac [rule'] i) st))
+ (Method.insert_tac more_facts i THEN resolve_tac ctxt [rule'] i) st))
end);
end;