src/HOL/Tools/Datatype/datatype_data.ML
changeset 38767 d8da44a8dd25
parent 38756 d07959fabde6
child 39557 fe5722fce758
     1.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Aug 27 00:09:56 2010 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Aug 27 12:40:20 2010 +0200
     1.3 @@ -257,7 +257,9 @@
     1.4             Pretty.str " =" :: Pretty.brk 1 ::
     1.5             flat (separate [Pretty.brk 1, Pretty.str "| "]
     1.6               (map (single o pretty_constr) cos)));
     1.7 -    in Thy_Output.output (Thy_Output.maybe_pretty_source (K pretty_datatype) src [()]) end);
     1.8 +    in
     1.9 +      Thy_Output.output ctxt (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()])
    1.10 +    end);
    1.11  
    1.12  
    1.13