--- a/src/HOL/Tools/recdef_package.ML Fri Jan 27 18:29:33 2006 +0100
+++ b/src/HOL/Tools/recdef_package.ML Fri Jan 27 19:03:02 2006 +0100
@@ -280,7 +280,7 @@
val tc = List.nth (tcs, i - 1) handle Subscript =>
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
- in IsarThy.theorem_i Drule.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
+ in IsarThy.theorem_i PureThy.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const;
val recdef_tc_i = gen_recdef_tc (K I) (K I);