# HG changeset patch
# User wenzelm
# Date 1369589355 -7200
# Node ID ba6b2876ef5ae2a13f963901dcc2be87ee787d36
# Parent  576aceb343dc9c656f9975c8686584e9a4c5e19b
more uniform context;

diff -r 576aceb343dc -r ba6b2876ef5a src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Sun May 26 19:27:32 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Sun May 26 19:29:15 2013 +0200
@@ -104,13 +104,12 @@
 
 fun case_tr err ctxt [t, u] =
       let
-        val thy = Proof_Context.theory_of ctxt;
+        val consts = Proof_Context.consts_of ctxt;
+        fun is_const s = can (Consts.the_constraint consts) (Consts.intern consts s);
 
-        fun is_const s =
-          Sign.declared_const thy (Proof_Context.intern_const ctxt s);
-
-        fun abs p tTs t = Syntax.const @{const_syntax case_abs} $
-          fold constrain_Abs tTs (absfree p t);
+        fun abs p tTs t =
+          Syntax.const @{const_syntax case_abs} $
+            fold constrain_Abs tTs (absfree p t);
 
         fun abs_pat (Const (@{syntax_const "_constrain"}, _) $ t $ tT) tTs =
               abs_pat t (tT :: tTs)