added code_abstype keyword

--- a/etc/isar-keywords.el	Fri Feb 19 09:35:18 2010 +0100
+++ b/etc/isar-keywords.el	Fri Feb 19 11:06:20 2010 +0100
@@ -55,6 +55,7 @@
     "classes"
     "classrel"
     "code_abort"
+    "code_abstype"
     "code_class"
     "code_const"
     "code_datatype"
@@ -537,6 +538,7 @@
 (defconst isar-keywords-theory-goal
   '("ax_specification"
     "boogie_vc"
+    "code_abstype"
     "code_pred"
     "corollary"
     "cpodef"

--- a/src/Pure/Isar/isar_syn.ML	Fri Feb 19 09:35:18 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 19 11:06:20 2010 +0100
@@ -479,6 +479,11 @@
   OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
     (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
 
+val _ =
+  OuterSyntax.command "code_abstype" "define abstract code type" K.thy_goal
+    (P.term -- P.term >> (fn (abs, rep) => Toplevel.print
+      o Toplevel.theory_to_proof (Code.add_abstype_cmd abs rep)));
+
 
 
 (** proof commands **)