# HG changeset patch
# User wenzelm
# Date 1162759482 -3600
# Node ID 16fb5afbf2285b2b5d47cd1bf33ae6bae1ff5875
# Parent  0c51cd55a79c89b9c9ffb3ae6257cc5f56202517
case_tr: do not intern already internal consts;

diff -r 0c51cd55a79c -r 16fb5afbf228 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sun Nov 05 21:44:41 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Sun Nov 05 21:44:42 2006 +0100
@@ -402,8 +402,12 @@
       val thy = Context.theory_of context;
       fun case_error s name ts = raise TERM ("Error in case expression" ^
         getOpt (Option.map (curry op ^ " for datatype ") name, "") ^ ":\n" ^ s, ts);
-      fun dest_case1 (Const ("_case1", _) $ t $ u) = (case strip_comb t of
-            (Const (s, _), ts) => (((perhaps o try o unprefix) Syntax.constN o Sign.intern_const thy) s, ts)
+      fun dest_case1 (Const ("_case1", _) $ t $ u) =
+          (case strip_comb t of
+            (Const (s, _), ts) =>
+              (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?*)
           | _ => case_error "Head is not a constructor" NONE [t, u], u)
         | dest_case1 t = raise TERM ("dest_case1", [t]);