src/Pure/ML/ml_compiler.ML
changeset 64660 ef85bb6491b3
parent 63806 c54a53ef1873
child 64661 84aea854dc3c
     1.1 --- a/src/Pure/ML/ml_compiler.ML	Fri Dec 23 11:19:28 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_compiler.ML	Fri Dec 23 11:21:38 2016 +0100
     1.3 @@ -109,8 +109,6 @@
     1.4        | reported loc (PolyML.PTrefId id) = reported_entity_id false (FixedInt.toLarge id) loc
     1.5        | reported loc (PolyML.PTtype types) = reported_types loc types
     1.6        | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
     1.7 -      | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
     1.8 -      | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
     1.9        | reported loc (PolyML.PTcompletions names) = reported_completions loc names
    1.10        | reported _ _ = I
    1.11      and reported_tree (loc, props) = fold (reported loc) props;