# HG changeset patch
# User wenzelm
# Date 1427644462 -7200
# Node ID 57820650bd11c79568327256ed5603daeba1c091
# Parent  5e77a35adc67d4795d738dc74fbc21c5f625bbb3
tuned;

diff -r 5e77a35adc67 -r 57820650bd11 src/HOL/Probability/measurable.ML
--- a/src/HOL/Probability/measurable.ML	Sun Mar 29 17:43:03 2015 +0200
+++ b/src/HOL/Probability/measurable.ML	Sun Mar 29 17:54:22 2015 +0200
@@ -147,8 +147,9 @@
   | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
   | indep _ _ _ = true;
 
-fun cnt_prefixes ctxt (Abs (n, T, t)) = let
-      fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
+fun cnt_prefixes ctxt (Abs (n, T, t)) =
+    let
+      fun is_countable ty = Sign.of_sort (Proof_Context.theory_of ctxt) (ty, @{sort countable})
       fun cnt_walk (Abs (ns, T, t)) Ts =
           map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
         | cnt_walk (f $ g) Ts = let