diff -r d80b2df54d31 -r a96320074298 src/HOL/Analysis/Measurable.thy --- a/src/HOL/Analysis/Measurable.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Analysis/Measurable.thy Sun Jan 06 15:04:34 2019 +0100 @@ -46,7 +46,7 @@ lemma pred_sets2: "A \ sets N \ f \ measurable M N \ pred M (\x. f x \ A)" by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric]) -ML_file "measurable.ML" +ML_file \measurable.ML\ attribute_setup measurable = \ Scan.lift (