src/Pure/General/binding.ML
changeset 61950 a2d4742b127f
parent 61877 276ad4354069
child 62241 a4a1f282bcd5
--- a/src/Pure/General/binding.ML	Mon Dec 28 16:29:39 2015 +0100
+++ b/src/Pure/General/binding.ML	Mon Dec 28 16:30:24 2015 +0100
@@ -16,6 +16,7 @@
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
   val set_pos: Position.T -> binding -> binding
+  val reset_pos: binding -> binding
   val name: bstring -> binding
   val name_of: binding -> bstring
   val map_name: (bstring -> bstring) -> binding -> binding
@@ -84,6 +85,7 @@
 fun set_pos pos =
   map_binding (fn (restricted, concealed, prefix, qualifier, name, _) =>
     (restricted, concealed, prefix, qualifier, name, pos));
+val reset_pos = set_pos Position.none;
 
 fun name name = make (name, Position.none);
 fun name_of (Binding {name, ...}) = name;