--- a/src/Pure/ML/ml_compiler.ML Fri Dec 23 11:19:28 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML Fri Dec 23 11:21:38 2016 +0100
@@ -109,8 +109,6 @@
| reported loc (PolyML.PTrefId id) = reported_entity_id false (FixedInt.toLarge id) loc
| reported loc (PolyML.PTtype types) = reported_types loc types
| reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
- | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
- | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
| reported loc (PolyML.PTcompletions names) = reported_completions loc names
| reported _ _ = I
and reported_tree (loc, props) = fold (reported loc) props;