# HG changeset patch
# User wenzelm
# Date 1163018714 -3600
# Node ID f1e3967d559a2d7fb5d32edd36de24d7a148eb2d
# Parent  9bffcdfd755360070b41970fe57d4cadce44d78c
case_tr': proper handling of authentic consts;

diff -r 9bffcdfd7553 -r f1e3967d559a src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Nov 08 21:45:13 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Nov 08 21:45:14 2006 +0100
@@ -408,7 +408,7 @@
               (case try (unprefix Syntax.constN) s of
                 SOME c => (c, ts)
               | NONE => (Sign.intern_const thy s, ts))
-          | (Free (s, _), ts) => (Sign.intern_const thy s, ts) (*FIXME?*)
+          | (Free (s, _), ts) => (Sign.intern_const thy s, ts)
           | _ => case_error "Head is not a constructor" NONE [t, u], u)
         | dest_case1 t = raise TERM ("dest_case1", [t]);
       fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
@@ -465,6 +465,8 @@
 fun case_tr' constrs context ts =
   if length ts <> length constrs + 1 then raise Match else
   let
+    val consts = Context.cases Sign.consts_of ProofContext.consts_of context;
+
     val (fs, x) = split_last ts;
     fun strip_abs 0 t = ([], t)
       | strip_abs i (Abs p) =
@@ -478,7 +480,7 @@
         (loose_bnos (strip_abs_body t))
       end;
     val cases = map (fn ((cname, dts), t) =>
-      (Sign.extern_const (Context.theory_of context) cname,
+      (Consts.extern_early consts cname,
        strip_abs (length dts) t, is_dependent (length dts) t))
       (constrs ~~ fs);
     fun count_cases (_, _, true) = I