# HG changeset patch
# User wenzelm
# Date 1518801955 -3600
# Node ID eb11d722e3ef18ce3ee767b260b14b1dfc8e3b9e
# Parent  d4cb46bc836048a1b4226e11c7a6cb6e80da42a3
tuned whitespace;

diff -r d4cb46bc8360 -r eb11d722e3ef src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Feb 16 18:25:35 2018 +0100
+++ b/src/Pure/Isar/class.ML	Fri Feb 16 18:25:55 2018 +0100
@@ -87,10 +87,12 @@
   Class_Data {consts = consts, base_sort = base_sort,
     base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
     of_class = of_class, axiom = axiom, defs = defs, operations = operations};
+
 fun map_class_data f (Class_Data {consts, base_sort, base_morph, export_morph, assm_intro,
     of_class, axiom, defs, operations}) =
   make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
     (defs, operations)));
+
 fun merge_class_data _ (Class_Data {consts = consts,
     base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
     of_class = of_class, axiom = axiom, defs = defs1, operations = operations1},