# HG changeset patch
# User haftmann
# Date 1399616017 -7200
# Node ID 1e50fddbe1f5973c8c76ebbd85ff2d64bb943b4c
# Parent  4044a7d1720f64fa101baf107766f14da2f65689
dropped term_of obfuscation -- not really required;
tuned theory structure

diff -r 4044a7d1720f -r 1e50fddbe1f5 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:37 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:37 2014 +0200
@@ -73,10 +73,19 @@
   shows "x \<equiv> y"
   using assms by simp
 
+code_printing
+  type_constructor "term" \<rightharpoonup> (Eval) "Term.term"
+| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))"
+| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))"
+| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
+| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
+
 ML_file "Tools/code_evaluation.ML"
 
 code_reserved Eval Code_Evaluation
 
+ML_file "~~/src/HOL/Tools/value.ML"
+
 
 subsection {* @{text term_of} instances *}
 
@@ -104,9 +113,6 @@
 
 end
 
-
-subsubsection {* Code generator setup *}
-
 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"]]
@@ -119,30 +125,15 @@
   by (subst term_of_anything) rule 
 
 code_printing
-  type_constructor "term" \<rightharpoonup> (Eval) "Term.term"
-| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))"
-| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))"
-| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
-| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
-| constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
+  constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
 | constant "term_of \<Colon> String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
 
 code_reserved Eval HOLogic
 
 
-subsubsection {* Obfuscation *}
+subsection {* Generic reification *}
 
-print_translation {*
-  let
-    val term = Const ("<TERM>", dummyT);
-    fun tr1' _ [_, _] = term;
-    fun tr2' _ [] = term;
-  in
-   [(@{const_syntax Const}, tr1'),
-    (@{const_syntax App}, tr1'),
-    (@{const_syntax dummy_term}, tr2')]
-  end
-*}
+ML_file "~~/src/HOL/Tools/reification.ML"
 
 
 subsection {* Diagnostic *}
@@ -154,16 +145,6 @@
   constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing"
 
 
-subsection {* Interactive evaluation *}
-
-ML_file "~~/src/HOL/Tools/value.ML"
-
-
-subsection {* Generic reification *}
-
-ML_file "~~/src/HOL/Tools/reification.ML"
-
-
 hide_const dummy_term valapp
 hide_const (open) Const App Abs Free termify valtermify term_of tracing