# HG changeset patch
# User wenzelm
# Date 1394184147 -3600
# Node ID 7644d63e8c3fe77ba4787135cda8141fc2595a34
# Parent  972f0aa7091b0c647c4e744e7ca2ebf53619a484
modernized theory setup;

diff -r 972f0aa7091b -r 7644d63e8c3f src/HOL/Ctr_Sugar.thy
--- a/src/HOL/Ctr_Sugar.thy	Fri Mar 07 01:02:21 2014 +0100
+++ b/src/HOL/Ctr_Sugar.thy	Fri Mar 07 10:22:27 2014 +0100
@@ -27,7 +27,6 @@
 declare [[coercion_args case_elem - +]]
 
 ML_file "Tools/Ctr_Sugar/case_translation.ML"
-setup Case_Translation.setup
 
 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
 by (erule iffI) (erule contrapos_pn)
diff -r 972f0aa7091b -r 7644d63e8c3f src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 07 01:02:21 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 07 10:22:27 2014 +0100
@@ -21,7 +21,6 @@
   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;
 
@@ -180,7 +179,7 @@
       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 *)
@@ -207,7 +206,7 @@
       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 *)
@@ -229,6 +228,12 @@
     |> 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 *)
 
@@ -453,8 +458,7 @@
     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 *)
@@ -595,21 +599,7 @@
   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 *)