# HG changeset patch
# User wenzelm
# Date 1361795462 -3600
# Node ID 3928173409e47467c3a832ec5b3e07cff4d77bd9
# Parent  cfc83ad52571ad06135bd4cf2bf3476e9854e210
reconsider 'export_code' as "thy_decl" command due to its global side-effect on the file-system;

diff -r cfc83ad52571 -r 3928173409e4 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Feb 25 13:29:19 2013 +0100
+++ b/etc/isar-keywords.el	Mon Feb 25 13:31:02 2013 +0100
@@ -383,7 +383,6 @@
     "code_deps"
     "code_thms"
     "display_drafts"
-    "export_code"
     "find_consts"
     "find_theorems"
     "find_unused_assms"
@@ -510,6 +509,7 @@
     "domain_isomorphism"
     "domaindef"
     "equivariance"
+    "export_code"
     "extract"
     "extract_type"
     "fixrec"
diff -r cfc83ad52571 -r 3928173409e4 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Mon Feb 25 13:29:19 2013 +0100
+++ b/src/Tools/Code_Generator.thy	Mon Feb 25 13:31:02 2013 +0100
@@ -7,8 +7,8 @@
 theory Code_Generator
 imports Pure
 keywords
-  "value" "print_codeproc" "code_thms" "code_deps" "export_code" :: diag and
-  "code_class" "code_instance" "code_type"
+  "value" "print_codeproc" "code_thms" "code_deps" :: diag and
+  "export_code" "code_class" "code_instance" "code_type"
     "code_const" "code_reserved" "code_include" "code_modulename"
     "code_abort" "code_monad" "code_reflect" :: thy_decl and
   "datatypes" "functions" "module_name" "file" "checking"