# HG changeset patch
# User wenzelm
# Date 1606308688 -3600
# Node ID 52d0b5fcb19d6a475a8304bf8ae396eb4a92b3a3
# Parent  0471eb6a4b99e397058ee8d7ecfe405a16a04f7e
unused;

diff -r 0471eb6a4b99 -r 52d0b5fcb19d src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Nov 25 13:30:06 2020 +0100
+++ b/src/Pure/General/position.ML	Wed Nov 25 13:51:28 2020 +0100
@@ -40,7 +40,6 @@
   val def_properties_of: T -> Properties.T
   val entity_markup: string -> string * T -> Markup.T
   val entity_properties_of: bool -> serial -> T -> Properties.T
-  val default_properties: T -> Properties.T -> Properties.T
   val markup: T -> Markup.T -> Markup.T
   val is_reported: T -> bool
   val is_reported_range: T -> bool
@@ -211,10 +210,6 @@
   if def then (Markup.defN, Value.print_int serial) :: properties_of pos
   else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
 
-fun default_properties default props =
-  if exists (member (op =) Markup.position_properties o #1) props then props
-  else properties_of default @ props;
-
 val markup = Markup.properties o properties_of;