src/Pure/Syntax/term_position.ML
changeset 49674 dbadb4d03cbc
parent 45666 d83797ef0d2d
child 49685 4341e4d86872
     1.1 --- a/src/Pure/Syntax/term_position.ML	Mon Oct 01 12:05:05 2012 +0200
     1.2 +++ b/src/Pure/Syntax/term_position.ML	Mon Oct 01 16:37:22 2012 +0200
     1.3 @@ -11,8 +11,10 @@
     1.4    val decode: string -> Position.T option
     1.5    val decode_position: term -> (Position.T * typ) option
     1.6    val decode_positionT: typ -> Position.T option
     1.7 +  val decode_positionS: sort -> Position.T option
     1.8    val is_position: term -> bool
     1.9    val is_positionT: typ -> bool
    1.10 +  val is_positionS: sort -> bool
    1.11    val strip_positions: term -> term
    1.12  end;
    1.13  
    1.14 @@ -50,11 +52,15 @@
    1.15  fun decode_positionT (TFree (x, _)) = decode x
    1.16    | decode_positionT _ = NONE;
    1.17  
    1.18 +fun decode_positionS [x] = decode x
    1.19 +  | decode_positionS _ = NONE;
    1.20 +
    1.21  val is_position = is_some o decode_position;
    1.22  val is_positionT = is_some o decode_positionT;
    1.23 +val is_positionS = is_some o decode_positionS;
    1.24  
    1.25  fun strip_positions ((t as Const (c, _)) $ u $ v) =
    1.26 -      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
    1.27 +      if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v
    1.28        then strip_positions u
    1.29        else t $ strip_positions u $ strip_positions v
    1.30    | strip_positions (t $ u) = strip_positions t $ strip_positions u