datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
authorwenzelm
Tue Mar 22 14:22:40 2011 +0100 (2011-03-22)
changeset 420505a505dfec04e
parent 42049 e945717b2b15
child 42051 dbdd4790da34
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
src/HOL/Tools/Datatype/datatype_case.ML
src/Pure/Syntax/type_ext.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Tue Mar 22 13:55:39 2011 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Tue Mar 22 14:22:40 2011 +0100
     1.3 @@ -339,7 +339,7 @@
     1.4            | dest_case1 t = case_error "dest_case1";
     1.5          fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
     1.6            | dest_case2 t = [t];
     1.7 -        val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
     1.8 +        val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 (Syntax.strip_positions u)));
     1.9          val (case_tm, _) = make_case_untyped (tab_of thy) ctxt
    1.10            (if err then Error else Warning) []
    1.11            (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
     2.1 --- a/src/Pure/Syntax/type_ext.ML	Tue Mar 22 13:55:39 2011 +0100
     2.2 +++ b/src/Pure/Syntax/type_ext.ML	Tue Mar 22 14:22:40 2011 +0100
     2.3 @@ -9,6 +9,7 @@
     2.4    val sort_of_term: term -> sort
     2.5    val term_sorts: term -> (indexname * sort) list
     2.6    val typ_of_term: (indexname -> sort) -> term -> typ
     2.7 +  val strip_positions: term -> term
     2.8    val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
     2.9      (string -> bool * string) -> (string -> string option) -> term -> term
    2.10    val term_of_typ: bool -> typ -> term
    2.11 @@ -101,11 +102,22 @@
    2.12    in typ_of tm end;
    2.13  
    2.14  
    2.15 -(* decode_term -- transform parse tree into raw term *)
    2.16 +(* positions *)
    2.17  
    2.18  fun is_position (Free (x, _)) = is_some (Lexicon.decode_position x)
    2.19    | is_position _ = false;
    2.20  
    2.21 +fun strip_positions ((t as Const (c, _)) $ u $ v) =
    2.22 +      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
    2.23 +      then strip_positions u
    2.24 +      else t $ strip_positions u $ strip_positions v
    2.25 +  | strip_positions (t $ u) = strip_positions t $ strip_positions u
    2.26 +  | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
    2.27 +  | strip_positions t = t;
    2.28 +
    2.29 +
    2.30 +(* decode_term -- transform parse tree into raw term *)
    2.31 +
    2.32  fun decode_term get_sort map_const map_free tm =
    2.33    let
    2.34      val decodeT = typ_of_term (get_sort (term_sorts tm));