# HG changeset patch
# User krauss
# Date 1307484080 -7200
# Node ID b142ae3e9478a0f2bca7dc242040ecf1a63ffba2
# Parent  f4d15a58ed8b8d08334b2360be42c0f33bc212e2
more precise type for obscure "prfx" field

diff -r f4d15a58ed8b -r b142ae3e9478 src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Tue Jun 07 21:37:40 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Wed Jun 08 00:01:20 2011 +0200
@@ -64,7 +64,7 @@
 fun row_of_pat x = fst (snd x);
 
 fun add_row_used ((prfx, pats), (tm, tag)) =
-  fold Term.add_free_names (tm :: pats @ prfx);
+  fold Term.add_free_names (tm :: pats @ map Free prfx);
 
 (* try to preserve names given by user *)
 fun default_names names ts =
@@ -172,10 +172,10 @@
       in (prfx, tag, list_comb (c', args) :: plist') end
   in map build l end;
 
-fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
+fun v_to_prfx (prfx, Free v::pats) = (v::prfx,pats)
   | v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
 
-fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
+fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, Free v::pats)
   | v_to_pats _ = raise CASE_ERROR ("mk_case: v_to_pats", ~1);