src/Pure/sign.ML

   val hide_space_i: string * string list -> sg -> sg
   val add_name: string -> sg -> sg
   val data_kinds: data -> string list
   val merge_refs: sg_ref * sg_ref -> sg_ref
   val merge: sg * sg -> sg
+  val copy: sg -> sg
+  val finish: sg -> sg
   val prep_ext: sg -> sg
-  val copy: sg -> sg
   val PureN: string
   val CPureN: string
   val nontriv_merge: sg * sg -> sg
   val pre_pure: sg
   val const_of_class: class -> string

 
 signature PRIVATE_SIGN =
 sig
   include SIGN
   val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
-    (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
+    (Object.T -> Object.T) * (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit))
+    -> sg -> sg
   val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
   val print_data: Object.kind -> sg -> unit
 end;
 

     data: data}                                 (*anytype data*)
 and data =
   Data of
     (Object.kind *                              (*kind (for authorization)*)
       (Object.T *                               (*value*)
-        ((Object.T -> Object.T) *               (*prepare extend method*)
-          (Object.T -> Object.T) *              (*copy method*)
+        ((Object.T -> Object.T) *               (*copy method*)
+          (Object.T -> Object.T) *              (*finish method*)
+          (Object.T -> Object.T) *              (*prepare extend method*)
           (Object.T * Object.T -> Object.T) *   (*merge and prepare extend method*)
           (sg -> Object.T -> unit))))           (*print method*)
     Symtab.table
 and sg_ref =
   SgRef of sg ref option;

    fun entry data kind =
      (case gen_assoc Object.eq_kind (data, kind) of
        None => []
      | Some x => [(kind, x)]);
 
-    fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] =
+    fun merge_entries [(kind, (e, mths as (_, _, ext, _, _)))] =
           (kind, (ext e handle exn => err_method "prep_ext" (Object.name_of_kind kind) exn, mths))
-      | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] =
+      | merge_entries [(kind, (e1, mths as (_, _, _, mrg, _))), (_, (e2, _))] =
           (kind, (mrg (e1, e2)
             handle exn => err_method "merge" (Object.name_of_kind kind) exn, mths))
       | merge_entries _ = sys_error "merge_entries";
 
     val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;

       handle Symtab.DUPS dups => err_inconsistent dups
   end;
 
 fun prep_ext_data data = merge_data (data, empty_data);
 
-fun init_data_sg sg (Data tab) kind e cp ext mrg prt =
+fun init_data_sg sg (Data tab) kind e cp fin ext mrg prt =
   let val name = Object.name_of_kind kind in
-    Data (Symtab.update_new ((name, (kind, (e, (cp, ext, mrg, prt)))), tab))
+    Data (Symtab.update_new ((name, (kind, (e, (cp, fin, ext, mrg, prt)))), tab))
       handle Symtab.DUP _ => err_dup_init sg name
   end;
 
 
 (* access data *)

 fun get_data kind f (sg as Sg (_, {data = Data tab, ...})) =
   let val x = fst (lookup_data sg tab kind)
   in f x handle Match => Object.kind_error kind end;
 
 fun print_data kind (sg as Sg (_, {data = Data tab, ...})) =
-  let val (e, (_, _, _, prt)) = lookup_data sg tab kind
+  let val (e, (_, _, _, _, prt)) = lookup_data sg tab kind
   in prt sg e handle exn => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn end;
 
 fun put_data_sg sg (Data tab) kind f x =
   Data (Symtab.update ((Object.name_of_kind kind,
     (kind, (f x, snd (lookup_data sg tab kind)))), tab));

   (syn, tsig, ctab, (path, hide_names spaces kind names), data);
 
 
 (* signature data *)
 
-fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, ext, mrg, prt)) =
-  (syn, tsig, ctab, names, init_data_sg sg data kind e cp ext mrg prt);
+fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, fin, ext, mrg, prt)) =
+  (syn, tsig, ctab, names, init_data_sg sg data kind e cp fin ext mrg prt);
 
 fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) =
   (syn, tsig, ctab, names, put_data_sg sg data kind f x);
 
 
-fun copy_data (k, (e, mths as (cp, _, _, _))) =
+fun finish_data (k, (e, mths as (_, fin, _, _, _))) =
+  (k, (fin e handle exn => err_method "finish" (Object.name_of_kind k) exn, mths));
+
+fun ext_finish_data (syn, tsig, ctab, names, Data tab) () =
+  (syn, tsig, ctab, names, Data (Symtab.map finish_data tab));
+
+
+fun copy_data (k, (e, mths as (cp, _, _, _, _))) =
   (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths));
 
 fun copy (sg as Sg ({id = _, stamps}, {self, tsig, const_tab, syn, path, spaces, data})) =
   let
     val _ = check_stale sg;

 val add_space         = extend_sign true ext_add_space "#";
 val hide_space        = extend_sign true ext_hide_space "#";
 val hide_space_i      = extend_sign true ext_hide_space_i "#";
 fun init_data arg sg  = extend_sign true (ext_init_data sg) "#" arg sg;
 fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg;
+fun finish sg         = extend_sign true ext_finish_data "#" () sg;
 fun add_name name sg  = extend_sign true K name () sg;
 fun prep_ext sg       = extend_sign false K "#" () sg;