src/Pure/Syntax/type_ext.ML
changeset 42052 34f1d2d81284
parent 42050 5a505dfec04e
child 42053 006095137a81
     1.1 --- a/src/Pure/Syntax/type_ext.ML	Tue Mar 22 14:45:48 2011 +0100
     1.2 +++ b/src/Pure/Syntax/type_ext.ML	Tue Mar 22 15:32:47 2011 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    val term_sorts: term -> (indexname * sort) list
     1.5    val typ_of_term: (indexname -> sort) -> term -> typ
     1.6    val strip_positions: term -> term
     1.7 +  val strip_positions_ast: Ast.ast -> Ast.ast
     1.8    val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
     1.9      (string -> bool * string) -> (string -> string option) -> term -> term
    1.10    val term_of_typ: bool -> typ -> term
    1.11 @@ -115,6 +116,13 @@
    1.12    | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
    1.13    | strip_positions t = t;
    1.14  
    1.15 +fun strip_positions_ast (Ast.Appl ((t as Ast.Constant c) :: u :: (v as Ast.Variable x) :: asts)) =
    1.16 +      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Lexicon.decode_position x)
    1.17 +      then Ast.mk_appl (strip_positions_ast u) (map strip_positions_ast asts)
    1.18 +      else Ast.Appl (map strip_positions_ast (t :: u :: v :: asts))
    1.19 +  | strip_positions_ast (Ast.Appl asts) = Ast.Appl (map strip_positions_ast asts)
    1.20 +  | strip_positions_ast ast = ast;
    1.21 +
    1.22  
    1.23  (* decode_term -- transform parse tree into raw term *)
    1.24