Removed code generator stuff. Code generation is now handled by code
authorberghofe
Tue Oct 26 16:29:54 2004 +0200 (2004-10-26)
changeset 15258b93efa469f92
parent 15257 19dcdea98649
child 15259 6aa593317905
Removed code generator stuff. Code generation is now handled by code
generator in typedef_package.
src/HOL/Tools/record_package.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Tue Oct 26 16:26:53 2004 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Tue Oct 26 16:29:54 2004 +0200
     1.3 @@ -1334,20 +1334,11 @@
     1.4            :== mk_ext args
     1.5        end;
     1.6      val upd_specs = map mk_upd_spec fields_more;
     1.7 -
     1.8 -    (* code generator data *)
     1.9 -        (* Representation as nested pairs is revealed for codegeneration *)
    1.10 -    val [rep_code,abs_code] = map (Codegen.parse_mixfix (K (Bound 0))) ["(_)","(_)"];
    1.11 -    val ext_type_code = Codegen.parse_mixfix (K dummyT) "(_)";
    1.12      
    1.13      (* 1st stage: defs_thy *)
    1.14      val (defs_thy, (([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs),upd_defs)) =
    1.15          thy 
    1.16          |> extension_typedef name repT (alphas@[zeta])
    1.17 -        |>> Codegen.assoc_consts_i 
    1.18 -               [(mk_AbsN name,None,abs_code),
    1.19 -                (mk_RepN name,None,rep_code)]
    1.20 -        |>> Codegen.assoc_types [(extT_name,ext_type_code)]
    1.21          |>> Theory.add_consts_i 
    1.22                (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
    1.23          |>>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))