1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Apr 11 16:51:06 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 11 16:51:07 2010 +0200
     1.3 @@ -480,11 +480,6 @@
     1.4    OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
     1.5      (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
     1.6  
     1.7 -val _ =
     1.8 -  OuterSyntax.command "code_abstype" "define abstract code type" K.thy_goal
     1.9 -    (P.term -- P.term >> (fn (abs, rep) => Toplevel.print
    1.10 -      o Toplevel.theory_to_proof (Code.add_abstype_cmd abs rep)));
    1.11 -
    1.12  
    1.13  
    1.14  (** proof commands **)