src/HOL/Tools/datatype_realizer.ML
changeset 24711 e8bba7723858
parent 24699 c6674504103f
child 24712 64ed05609568
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 13:42:59 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 15:34:35 2007 +0200
     1.3 @@ -228,6 +228,6 @@
     1.4      |> fold_rev (make_casedists (#sorts info)) infos
     1.5    end;
     1.6  
     1.7 -val setup = DatatypePackage.add_interpretator add_dt_realizers;
     1.8 +val setup = DatatypePackage.interpretation add_dt_realizers;
     1.9  
    1.10  end;