uniform Term_Position.markers (cf. dbadb4d03cbc);

--- a/src/Pure/Syntax/ast.ML	Mon May 27 10:13:51 2013 +0200
+++ b/src/Pure/Syntax/ast.ML	Mon May 27 12:40:50 2013 +0200
@@ -70,7 +70,7 @@
 (* strip_positions *)
 
 fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) =
-      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Term_Position.decode x)
+      if member (op =) Term_Position.markers c andalso is_some (Term_Position.decode x)
       then mk_appl (strip_positions u) (map strip_positions asts)
       else Appl (map strip_positions (t :: u :: v :: asts))
   | strip_positions (Appl asts) = Appl (map strip_positions asts)

--- a/src/Pure/Syntax/term_position.ML	Mon May 27 10:13:51 2013 +0200
+++ b/src/Pure/Syntax/term_position.ML	Mon May 27 12:40:50 2013 +0200
@@ -14,6 +14,7 @@
   val decode_positionS: sort -> Position.T list * sort
   val is_position: term -> bool
   val is_positionT: typ -> bool
+  val markers: string list
   val strip_positions: term -> term
 end;
 
@@ -58,8 +59,10 @@
 val is_position = is_some o decode_position;
 val is_positionT = is_some o decode_positionT;
 
+val markers = ["_constrain", "_constrainAbs", "_ofsort"];
+
 fun strip_positions ((t as Const (c, _)) $ u $ v) =
-      if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v
+      if member (op =) markers c andalso is_position v
       then strip_positions u
       else t $ strip_positions u $ strip_positions v
   | strip_positions (t $ u) = strip_positions t $ strip_positions u