--- a/src/Tools/Code/code_eval.ML Sat Feb 06 23:26:17 2010 +0100
+++ b/src/Tools/Code/code_eval.ML Sun Feb 07 18:04:48 2010 +0100
@@ -107,25 +107,25 @@
val _ = map2 check_base constrs constrs'';
in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end;
-fun print_code struct_name is_first print_it ctxt =
+fun print_code is_first print_it ctxt =
let
val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
val ml_code = if is_first then ml_code
else "";
- val all_struct_name = Long_Name.append struct_name struct_code_name;
+ val all_struct_name = "Isabelle." ^ struct_code_name;
in (ml_code, print_it all_struct_name tycos_map consts_map) end;
in
-fun ml_code_antiq raw_const {struct_name, background} =
+fun ml_code_antiq raw_const background =
let
val const = Code.check_const (ProofContext.theory_of background) raw_const;
val is_first = is_first_occ background;
val background' = register_const const background;
- in (print_code struct_name is_first (print_const const), background') end;
+ in (print_code is_first (print_const const), background') end;
-fun ml_code_datatype_antiq (raw_tyco, raw_constrs) {struct_name, background} =
+fun ml_code_datatype_antiq (raw_tyco, raw_constrs) background =
let
val thy = ProofContext.theory_of background;
val tyco = Sign.intern_type thy raw_tyco;
@@ -135,7 +135,7 @@
else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
val is_first = is_first_occ background;
val background' = register_datatype tyco constrs background;
- in (print_code struct_name is_first (print_datatype tyco constrs), background') end;
+ in (print_code is_first (print_datatype tyco constrs), background') end;
end; (*local*)