--- a/src/HOL/Tools/inductive_package.ML Tue Nov 14 00:15:37 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML Tue Nov 14 00:15:38 2006 +0100
@@ -766,7 +766,7 @@
(s, SOME (ProofContext.infer_type ctxt' s))) pnames_syn;
val cnames_syn' = map (fn (s, _, mx) =>
(s, SOME (ProofContext.infer_type ctxt' s), mx)) cnames_syn;
- val (monos, ctxt'') = LocalTheory.theory_result (IsarThy.apply_theorems raw_monos) ctxt;
+ val (monos, ctxt'') = LocalTheory.theory_result (IsarCmd.apply_theorems raw_monos) ctxt;
in
add_inductive_i verbose "" coind false false cnames_syn' pnames intrs monos ctxt''
end;