# HG changeset patch
# User bulwahn
# Date 1316441899 -7200
# Node ID f12ef61ea76e1aca06f175b47a682002107fa26d
# Parent  e534939f880d6eaddc9b6e96818c3cb346113d82
determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations

diff -r e534939f880d -r f12ef61ea76e src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:19 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:19 2011 +0200
@@ -581,6 +581,11 @@
 
 (* inference of type annotations for disambiguation with type classes *)
 
+fun dest_tagged_type (Type ("", [T])) = (true, T)
+  | dest_tagged_type T = (false, T)
+
+val untag_term = map_types (snd o dest_tagged_type)
+
 fun annotate_term (proj_sort, _) eqngr =
   let
     val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr
@@ -786,7 +791,7 @@
     val tys = arg_types num_args (snd c_ty);
     val ty = nth tys t_pos;
     fun mk_constr c t = let val n = Code.args_number thy c
-      in ((c, arg_types n (fastype_of t) ---> ty), n) end;
+      in ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
     val constrs = if null case_pats then []
       else map2 mk_constr case_pats (nth_drop t_pos ts);
     fun casify naming constrs ty ts =