src/HOL/Tools/Datatype/datatype.ML
changeset 33314 53d49370f7af
parent 33313 f6acebef3ea1
child 33368 b1cf34f1855c
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 16:09:41 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 16:15:33 2009 +0100
     1.3 @@ -263,7 +263,7 @@
     1.4  
     1.5  (** abstract theory extensions relative to a datatype characterisation **)
     1.6  
     1.7 -structure Datatype_Interpretation = InterpretationFun
     1.8 +structure Datatype_Interpretation = Interpretation
     1.9    (type T = config * string list val eq: T * T -> bool = eq_snd op =);
    1.10  fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
    1.11