src/HOL/Tools/datatype_package.ML
changeset 21350 6e58289b6685
parent 21253 f1e3967d559a
child 21419 809e7520234a
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Nov 14 00:15:37 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Nov 14 00:15:38 2006 +0100
     1.3 @@ -921,8 +921,8 @@
     1.4        simps = simps}, thy11)
     1.5    end;
     1.6  
     1.7 -val rep_datatype = gen_rep_datatype IsarThy.apply_theorems;
     1.8 -val rep_datatype_i = gen_rep_datatype IsarThy.apply_theorems_i;
     1.9 +val rep_datatype = gen_rep_datatype IsarCmd.apply_theorems;
    1.10 +val rep_datatype_i = gen_rep_datatype IsarCmd.apply_theorems_i;
    1.11  
    1.12  
    1.13