# 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));