src/HOL/Tools/Ctr_Sugar/case_translation.ML

   val make_case:  Proof.context -> config -> Name.context -> term -> (term * term) list -> term
   val print_case_translations: Proof.context -> unit
   val strip_case: Proof.context -> bool -> term -> (term * (term * term) list) option
   val strip_case_full: Proof.context -> bool -> term -> term
   val show_cases: bool Config.T
-  val setup: theory -> theory
   val register: term -> term list -> Context.generic -> Context.generic
 end;
 
 structure Case_Translation: CASE_TRANSLATION =
 struct

             (dest_case2 u)
             (Syntax.const @{const_syntax case_nil}))
       end
   | case_tr _ _ _ = case_error "case_tr";
 
-val trfun_setup = Sign.parse_translation [(@{syntax_const "_case_syntax"}, case_tr true)];
+val _ = Theory.setup (Sign.parse_translation [(@{syntax_const "_case_syntax"}, case_tr true)]);
 
 
 (* print translation *)
 
 fun case_tr' (_ :: x :: t :: ts) =

           foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
             (mk_clauses t), ts)
       end
   | case_tr' _ = raise Match;
 
-val trfun_setup' = Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')];
+val _ = Theory.setup (Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')]);
 
 
 (* declarations *)
 
 fun register raw_case_comb raw_constrs context =

   in
     context
     |> map_constrs update_constrs
     |> map_cases update_cases
   end;
+
+val _ = Theory.setup
+  (Attrib.setup @{binding case_translation}
+    (Args.term -- Scan.repeat1 Args.term >>
+      (fn (t, ts) => Thm.declaration_attribute (K (register t ts))))
+    "declaration of case combinators and constructors");
 
 
 (* (Un)check phases *)
 
 datatype config = Error | Warning | Quiet;

       | decode_case t = t;
   in
     map decode_case
   end;
 
-val term_check_setup =
-  Context.theory_map (Syntax_Phases.term_check 1 "case" check_case);
+val _ = Context.>> (Syntax_Phases.term_check 1 "case" check_case);
 
 
 (* Pretty printing of nested case expressions *)
 
 (* destruct one level of pattern matching *)

 fun uncheck_case ctxt ts =
   if Config.get ctxt show_cases
   then map (fn t => if can Term.type_of t then strip_case_full ctxt true t else t) ts
   else ts;
 
-val term_uncheck_setup =
-  Context.theory_map (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
-
-
-(* theory setup *)
-
-val setup =
-  trfun_setup #>
-  trfun_setup' #>
-  term_check_setup #>
-  term_uncheck_setup #>
-  Attrib.setup @{binding case_translation}
-    (Args.term -- Scan.repeat1 Args.term >>
-      (fn (t, ts) => Thm.declaration_attribute (K (register t ts))))
-    "declaration of case combinators and constructors";
+val _ = Context.>>  (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
 
 
 (* outer syntax commands *)
 
 fun print_case_translations ctxt =