--- a/src/HOL/Tools/Datatype/datatype_case.ML Tue Mar 22 18:03:28 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Tue Mar 22 20:44:47 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 (Syntax.strip_positions u)));
+ val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 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)