--- a/src/Pure/General/binding.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/General/binding.ML Fri Aug 09 17:14:49 2019 +0200
@@ -18,6 +18,7 @@
val set_pos: Position.T -> binding -> binding
val reset_pos: binding -> binding
val default_pos: binding -> binding
+ val default_pos_of: binding -> Position.T
val name: bstring -> binding
val name_of: binding -> bstring
val map_name: (bstring -> bstring) -> binding -> binding
@@ -95,6 +96,10 @@
fun default_pos b =
if pos_of b = Position.none then set_pos (Position.thread_data ()) b else b;
+fun default_pos_of b =
+ let val pos = pos_of b
+ in if pos = Position.none then Position.thread_data () else pos end;
+
(* name *)