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