# HG changeset patch # User wenzelm # Date 1300800160 -3600 # Node ID 5a505dfec04ec52f32edd1ac41bb33e5156f77f4 # Parent e945717b2b155a6ec77e1ab1e5f2cbb06dcbce5b datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn"; diff -r e945717b2b15 -r 5a505dfec04e src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Tue Mar 22 13:55:39 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Tue Mar 22 14:22:40 2011 +0100 @@ -339,7 +339,7 @@ | dest_case1 t = case_error "dest_case1"; fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u | dest_case2 t = [t]; - val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u)); + val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 (Syntax.strip_positions u))); val (case_tm, _) = make_case_untyped (tab_of thy) ctxt (if err then Error else Warning) [] (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT) diff -r e945717b2b15 -r 5a505dfec04e src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Tue Mar 22 13:55:39 2011 +0100 +++ b/src/Pure/Syntax/type_ext.ML Tue Mar 22 14:22:40 2011 +0100 @@ -9,6 +9,7 @@ val sort_of_term: term -> sort val term_sorts: term -> (indexname * sort) list val typ_of_term: (indexname -> sort) -> term -> typ + val strip_positions: term -> term val decode_term: (((string * int) * sort) list -> string * int -> sort) -> (string -> bool * string) -> (string -> string option) -> term -> term val term_of_typ: bool -> typ -> term @@ -101,11 +102,22 @@ in typ_of tm end; -(* decode_term -- transform parse tree into raw term *) +(* positions *) fun is_position (Free (x, _)) = is_some (Lexicon.decode_position x) | is_position _ = false; +fun strip_positions ((t as Const (c, _)) $ u $ v) = + if (c = "_constrain" orelse c = "_constrainAbs") 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 + | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t) + | strip_positions t = t; + + +(* decode_term -- transform parse tree into raw term *) + fun decode_term get_sort map_const map_free tm = let val decodeT = typ_of_term (get_sort (term_sorts tm));