# HG changeset patch # User wenzelm # Date 1369651250 -7200 # Node ID 626a757d3c2d925778a52eef4f7982b4a461f1b4 # Parent 785d39ee875397079a06baa0d616373ac40cd260 uniform Term_Position.markers (cf. dbadb4d03cbc); diff -r 785d39ee8753 -r 626a757d3c2d src/Pure/Syntax/ast.ML --- 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) diff -r 785d39ee8753 -r 626a757d3c2d src/Pure/Syntax/term_position.ML --- 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