--- a/src/Tools/Code_Generator.thy Thu Jan 08 18:23:29 2015 +0100
+++ b/src/Tools/Code_Generator.thy Fri Jan 09 08:36:59 2015 +0100
@@ -16,15 +16,6 @@
ML_file "~~/src/Tools/cache_io.ML"
ML_file "~~/src/Tools/Code/code_preproc.ML"
-
-attribute_setup code_preproc_trace = {*
- (Scan.lift (Args.$$$ "off" >> K Code_Preproc.trace_none)
- || (Scan.lift (Args.$$$ "only" |-- Args.colon |-- Scan.repeat1 Parse.term))
- >> Code_Preproc.trace_only_ext
- || Scan.succeed Code_Preproc.trace_all)
- >> (Thm.declaration_attribute o K)
-*} "tracing of the code generator preprocessor"
-
ML_file "~~/src/Tools/Code/code_symbol.ML"
ML_file "~~/src/Tools/Code/code_thingol.ML"
ML_file "~~/src/Tools/Code/code_simp.ML"
@@ -35,14 +26,6 @@
ML_file "~~/src/Tools/Code/code_haskell.ML"
ML_file "~~/src/Tools/Code/code_scala.ML"
-setup {*
- Code_Simp.setup
- #> Code_Target.setup
- #> Code_ML.setup
- #> Code_Haskell.setup
- #> Code_Scala.setup
-*}
-
code_datatype "TYPE('a\<Colon>{})"
definition holds :: "prop" where