# HG changeset patch
# User haftmann
# Date 1399616016 -7200
# Node ID aaea99edc040faef335c0fef58f20b634f2cd8c5
# Parent  601edd9a68597365f53aea5a3fb8af4ceaf90c88
modernized setups

diff -r 601edd9a6859 -r aaea99edc040 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:36 2014 +0200
@@ -77,8 +77,6 @@
 
 code_reserved Eval Code_Evaluation
 
-setup {* Code_Evaluation.setup *}
-
 
 subsection {* @{text term_of} instances *}
 
@@ -109,16 +107,9 @@
 
 subsubsection {* Code generator setup *}
 
-lemmas [code del] = term.rec term.case term.size
-lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
-
-lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term)
-  = Code_Evaluation.term_of" ..
-lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term)
-  = Code_Evaluation.term_of" ..
+declare [[code drop: rec_term case_term size_term "size :: term \<Rightarrow> _" "HOL.equal :: term \<Rightarrow> _"
+  "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
+  "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
 
 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
   "Code_Evaluation.term_of c = (case c of Char x y \<Rightarrow>
@@ -168,8 +159,7 @@
 ML_file "~~/src/HOL/Tools/value.ML"
 
 setup {*
-  Value.setup
-  #> Value.add_evaluator ("nbe", Nbe.dynamic_value)
+  Value.add_evaluator ("nbe", Nbe.dynamic_value)
   #> Value.add_evaluator ("code", Code_Evaluation.dynamic_value_strict)
 *}
 
diff -r 601edd9a6859 -r aaea99edc040 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Fri May 09 08:13:36 2014 +0200
@@ -16,7 +16,6 @@
   val static_conv: Proof.context -> string list -> typ list -> Proof.context -> conv
   val put_term: (unit -> term) -> Proof.context -> Proof.context
   val tracing: string -> 'a -> 'a
-  val setup: theory -> theory
 end;
 
 structure Code_Evaluation : CODE_EVALUATION =
@@ -129,6 +128,15 @@
   in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
 
 
+(* setup *)
+
+val _ = Context.>> (Context.map_theory
+  (Code.datatype_interpretation ensure_term_of
+  #> Code.abstype_interpretation ensure_term_of
+  #> Code.datatype_interpretation ensure_term_of_code
+  #> Code.abstype_interpretation ensure_abs_term_of_code));
+
+
 (** termifying syntax **)
 
 fun map_default f xs =
@@ -155,6 +163,8 @@
 fun check_termify ctxt ts =
   the_default ts (map_default subst_termify ts);
 
+val _ = Context.>> (Syntax_Phases.term_check 0 "termify" check_termify);
+
 
 (** evaluation **)
 
@@ -220,14 +230,4 @@
 
 fun tracing s x = (Output.tracing s; x);
 
-
-(** setup **)
-
-val setup =
-  Code.datatype_interpretation ensure_term_of
-  #> Code.abstype_interpretation ensure_term_of
-  #> Code.datatype_interpretation ensure_term_of_code
-  #> Code.abstype_interpretation ensure_abs_term_of_code
-  #> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify);
-
 end;
diff -r 601edd9a6859 -r aaea99edc040 src/HOL/Tools/value.ML
--- a/src/HOL/Tools/value.ML	Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Tools/value.ML	Fri May 09 08:13:36 2014 +0200
@@ -10,7 +10,6 @@
   val value_select: string -> Proof.context -> term -> term
   val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
   val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
-  val setup : theory -> theory
 end;
 
 structure Value : VALUE =
@@ -67,13 +66,11 @@
     (opt_evaluator -- opt_modes -- Parse.term
       >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
 
-val antiq_setup =
-  Thy_Output.antiquotation @{binding value}
+val _ = Context.>> (Context.map_theory
+  (Thy_Output.antiquotation @{binding value}
     (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
     (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
       (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
-        [style (value_maybe_select some_name context t)]));
-
-val setup = antiq_setup;
+        [style (value_maybe_select some_name context t)]))));
 
 end;