src/HOL/Tools/datatype_package.ML
changeset 21350 6e58289b6685
parent 21253 f1e3967d559a
child 21419 809e7520234a
--- a/src/HOL/Tools/datatype_package.ML	Tue Nov 14 00:15:37 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Nov 14 00:15:38 2006 +0100
@@ -921,8 +921,8 @@
       simps = simps}, thy11)
   end;
 
-val rep_datatype = gen_rep_datatype IsarThy.apply_theorems;
-val rep_datatype_i = gen_rep_datatype IsarThy.apply_theorems_i;
+val rep_datatype = gen_rep_datatype IsarCmd.apply_theorems;
+val rep_datatype_i = gen_rep_datatype IsarCmd.apply_theorems_i;