--- a/src/Pure/defs.ML Tue May 31 17:52:10 2005 +0200
+++ b/src/Pure/defs.ML Tue May 31 19:32:41 2005 +0200
@@ -14,11 +14,17 @@
exception DEFS of string
exception CIRCULAR of (typ * string * string) list
exception INFINITE_CHAIN of (typ * string * string) list
+ exception FINAL of string * typ
exception CLASH of string * string * string
val empty : graph
- val declare : graph -> string -> typ -> graph (* exception DEFS *)
- val define : graph -> string -> typ -> string -> (string * typ) list -> graph (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH *)
+ val declare : graph -> string * typ -> graph (* exception DEFS *)
+ val define : graph -> string * typ -> string -> (string * typ) list -> graph
+ (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)
+
+ val finalize : graph -> string * typ -> graph (* exception DEFS *)
+
+ val finals : graph -> (typ list) Symtab.table
(* the first argument should be the smaller graph *)
val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
@@ -37,33 +43,26 @@
* defnode Symtab.table (* a table of defnodes, each corresponding to 1 definition of the constant for a particular type,
indexed by axiom name *)
* backref Symtab.table (* a table of all back references to this node, indexed by node name *)
+ * typ list (* a list of all finalized types *)
and defnode = Defnode of
typ (* type of the constant in this particular definition *)
* ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *)
and backref = Backref of
- noderef (* a reference to the node that has defnodes which reference a certain node A *)
+ noderef (* the name of the node that has defnodes which reference a certain node A *)
* (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *)
fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
-fun get_nodename (Node (n, _, _ ,_)) = n
-fun get_nodedefs (Node (_, _, defs, _)) = defs
-fun get_defnode (Node (_, _, defs, _)) defname = Symtab.lookup (defs, defname)
+fun get_nodename (Node (n, _, _ ,_, _)) = n
+fun get_nodedefs (Node (_, _, defs, _, _)) = defs
+fun get_defnode (Node (_, _, defs, _, _)) defname = Symtab.lookup (defs, defname)
fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
-fun get_nodename (Node (n, _, _ ,_)) = n
-
+fun get_nodename (Node (n, _, _ , _, _)) = n
-(*fun t2list t = rev (Symtab.foldl (fn (l, d) => d::l) ([], t))
-fun tmap f t = map (fn (a,b) => (a, f b)) t
-fun defnode2data (Defnode (typ, table)) = ("Defnode", typ, t2list table)
-fun backref2data (Backref (noderef, table)) = ("Backref", noderef, map fst (t2list table))
-fun node2data (Node (s, t, defs, backs)) = ("Node", ("nodename", s), ("nodetyp", t),
- ("defs", tmap defnode2data (t2list defs)), ("backs", tmap backref2data (t2list backs)))
-fun graph2data g = ("Graph", tmap node2data (t2list g))
-*)
-
-datatype graphaction = Declare of string * typ | Define of string * typ * string * (string * typ) list
+datatype graphaction = Declare of string * typ
+ | Define of string * typ * string * (string * typ) list
+ | Finalize of string * typ
type graph = (graphaction list) * (node Symtab.table)
@@ -73,13 +72,14 @@
exception CIRCULAR of (typ * string * string) list;
exception INFINITE_CHAIN of (typ * string * string) list;
exception CLASH of string * string * string;
+exception FINAL of string * typ;
fun def_err s = raise (DEFS s)
-fun declare (actions, g) name ty =
- ((Declare (name, ty))::actions,
- Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty)), g))
- handle Symtab.DUP _ => def_err "declare: constant is already defined"
+fun declare (actions, g) (cty as (name, ty)) =
+ ((Declare cty)::actions,
+ Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty, [])), g))
+ handle Symtab.DUP _ => def_err "constant is already declared"
fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;
@@ -216,7 +216,7 @@
Symtab.foldl g (a, def_edges)
end
-fun define (actions, graph) name ty axname body =
+fun define (actions, graph) (name, ty) axname body =
let
val ty = checkT ty
val body = map (fn (n,t) => (n, checkT t)) body
@@ -224,15 +224,22 @@
val mainnode = (case Symtab.lookup (graph, mainref) of
NONE => def_err ("constant "^(quote mainref)^" is not declared")
| SOME n => n)
- val (Node (n, gty, defs, backs)) = mainnode
+ val (Node (n, gty, defs, backs, finals)) = mainnode
val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
fun check_def (s, Defnode (ty', _)) =
(if can_be_unified_r ty ty' then
raise (CLASH (mainref, axname, s))
else if s = axname then
def_err "name of axiom is already used for another definition of this constant"
- else true)
+ else true)
val _ = forall_table check_def defs
+ fun check_final finalty =
+ (if can_be_unified_r finalty ty then
+ raise (FINAL (mainref, finalty))
+ else
+ true)
+ val _ = forall check_final finals
+
(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
(* body contains the constants that this constant definition depends on. For each element of body,
@@ -244,7 +251,7 @@
(case Symtab.lookup (graph, bodyn) of
NONE => def_err "body of constant definition references undeclared constant"
| SOME x => x)
- val (Node (_, general_btyp, bdefs, bbacks)) = bnode
+ val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode
in
case unify_r 0 bodyty general_btyp of
NONE => NONE
@@ -260,13 +267,13 @@
(case unify_r 0 bodyty def_ty of
NONE => (swallowed, l)
| SOME (maxidx, sigma1, sigma2) =>
- (is_instance bodyty def_ty,
+ (is_instance_r bodyty def_ty,
merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
val (swallowed, edges) = Symtab.foldl make_edges ((false, []), bdefs)
in
- if swallowed then
+ if swallowed orelse (exists (is_instance_r bodyty) bfinals) then
(bodyn, edges)
- else
+ else
(bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
end)
end
@@ -339,8 +346,8 @@
fun install_backref graph noderef pointingnoderef pointingdefname =
let
- val (Node (pname, _, _, _)) = getnode graph pointingnoderef
- val (Node (name, ty, defs, backs)) = getnode graph noderef
+ val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
+ val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
in
case Symtab.lookup (backs, pname) of
NONE =>
@@ -348,14 +355,14 @@
val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
in
- Symtab.update ((name, Node (name, ty, defs, backs)), graph)
+ Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
end
| SOME (Backref (pointingnoderef, defnames)) =>
let
val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
in
- Symtab.update ((name, Node (name, ty, defs, backs)), graph)
+ Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
end
handle Symtab.DUP _ => graph
end
@@ -368,8 +375,9 @@
val graph = Symtab.foldl install_backrefs (graph, edges)
- val (Node (_, _, _, backs)) = getnode graph mainref
- val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new ((axname, thisDefnode), defs), backs)), graph)
+ val (Node (_, _, _, backs, _)) = getnode graph mainref
+ val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new
+ ((axname, thisDefnode), defs), backs, finals)), graph)
(* Now we have to check all backreferences to this node and inform them about the new defnode.
In this section we also check for circularity. *)
@@ -420,7 +428,7 @@
in
(defnames, (defname, none_edges, this_edges)::newedges)
end
- | _ => def_err "update_defs, internal error, corrupt backrefs"
+ | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
end
val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
@@ -440,13 +448,14 @@
(* If a Circular exception is thrown then we never reach this point. *)
(* Ok, the definition is consistent, let's update this node. *)
- val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update ((axname, thisDefnode), defs), backs)), graph)
+ val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update
+ ((axname, thisDefnode), defs), backs, finals)), graph)
(* Furthermore, update all the other nodes that backreference this node. *)
fun final_update_backrefs graph noderef defname none_edges this_edges =
let
val node = getnode graph noderef
- val (Node (nodename, nodety, defs, backs)) = node
+ val (Node (nodename, nodety, defs, backs, finals)) = node
val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
@@ -467,7 +476,7 @@
val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
in
- Symtab.update ((nodename, Node (nodename, nodety, defs', backs)), graph)
+ Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
end
val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
@@ -477,18 +486,78 @@
((Define (name, ty, axname, body))::actions, graph)
end
+ fun finalize' ((c, ty), graph) =
+ case Symtab.lookup (graph, c) of
+ NONE => def_err ("finalize: constant "^(quote c)^" is not declared")
+ | SOME (Node (noderef, nodety, defs, backs, finals)) =>
+ let
+ val nodety = checkT nodety
+ in
+ if (not (is_instance_r ty nodety)) then
+ def_err ("finalize: only type instances of the declared constant "^(quote c)^" can be finalized")
+ else if exists (is_instance_r ty) finals then
+ graph
+ else
+ let
+ val finals = ty :: finals
+ val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
+ fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
+ let
+ fun update_backdef ((graph, defnames), (backdefname, _)) =
+ let
+ val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
+ val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)
+ val (defnames', all_edges') =
+ case Symtab.lookup (all_edges, noderef) of
+ NONE => sys_error "finalize: corrupt backref"
+ | SOME (_, (NONE, edges)::rest) =>
+ let
+ val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
+ in
+ if edges' = [] then
+ (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
+ else
+ (Symtab.update ((backdefname, ()), defnames),
+ Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
+ end
+ val defnode' = Defnode (def_ty, all_edges')
+ val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs),
+ backbacks, backfinals)
+ in
+ (Symtab.update ((backrefname, backnode'), graph), defnames')
+ end
+
+ val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
+ in
+ (graph', if Symtab.is_empty defnames' then backs
+ else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
+ end
+ val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
+ val Node (_, _, defs, _, _) = getnode graph' noderef
+ in
+ Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph')
+ end
+ end
+
+ fun finalize (history, graph) c_ty = ((Finalize c_ty)::history, finalize' (c_ty, graph))
- fun merge' (Declare (name, ty), g) = (declare g name ty handle _ => g)
+ fun merge' (Declare cty, g) = (declare g cty handle _ => g)
| merge' (Define (name, ty, axname, body), g as (_, graph)) =
(case Symtab.lookup (graph, name) of
- NONE => define g name ty axname body
- | SOME (Node (_, _, defs, _)) =>
+ NONE => define g (name, ty) axname body
+ | SOME (Node (_, _, defs, _, _)) =>
(case Symtab.lookup (defs, axname) of
- NONE => define g name ty axname body
+ NONE => define g (name, ty) axname body
| SOME _ => g))
+ | merge' (Finalize finals, g) = (finalize g finals handle _ => g)
fun merge (actions, _) g = foldr merge' g actions
+ fun finals (history, graph) =
+ Symtab.foldl
+ (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))
+ (Symtab.empty, graph)
+
end;
--- a/src/Pure/theory.ML Tue May 31 17:52:10 2005 +0200
+++ b/src/Pure/theory.ML Tue May 31 19:32:41 2005 +0200
@@ -4,7 +4,6 @@
The abstract type "theory" of theories.
*)
-
signature BASIC_THEORY =
sig
type theory
@@ -12,7 +11,6 @@
val rep_theory: theory ->
{sign: Sign.sg,
const_deps: Defs.graph,
- final_consts: typ list Symtab.table,
axioms: term Symtab.table,
oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
parents: theory list,
@@ -131,14 +129,13 @@
Theory of {
sign: Sign.sg,
const_deps: Defs.graph,
- final_consts: typ list Symtab.table,
axioms: term Symtab.table,
oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
parents: theory list,
ancestors: theory list};
-fun make_theory sign const_deps final_consts axioms oracles parents ancestors =
- Theory {sign = sign, const_deps = const_deps, final_consts = final_consts, axioms = axioms,
+fun make_theory sign const_deps axioms oracles parents ancestors =
+ Theory {sign = sign, const_deps = const_deps, axioms = axioms,
oracles = oracles, parents = parents, ancestors = ancestors};
fun rep_theory (Theory args) = args;
@@ -167,7 +164,7 @@
(*partial Pure theory*)
val pre_pure =
- make_theory Sign.pre_pure Defs.empty Symtab.empty Symtab.empty Symtab.empty [] [];
+ make_theory Sign.pre_pure Defs.empty Symtab.empty Symtab.empty [] [];
@@ -186,9 +183,9 @@
fun err_dup_oras names =
error ("Duplicate oracles: " ^ commas_quote names);
-fun ext_theory thy ext_sg ext_deps new_axms new_oras =
+fun ext_theory thy ext_sg new_axms new_oras =
let
- val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
+ val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
val draft = Sign.is_draft sign;
val axioms' =
Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
@@ -199,13 +196,13 @@
val (parents', ancestors') =
if draft then (parents, ancestors) else ([thy], thy :: ancestors);
in
- make_theory (ext_sg sign) (ext_deps const_deps) final_consts axioms' oracles' parents' ancestors'
+ make_theory (ext_sg sign) const_deps axioms' oracles' parents' ancestors'
end;
(* extend signature of a theory *)
-fun ext_sign ext_sg args thy = ext_theory thy (ext_sg args) I [] [];
+fun ext_sign ext_sg args thy = ext_theory thy (ext_sg args) [] [];
val add_classes = ext_sign Sign.add_classes;
val add_classes_i = ext_sign Sign.add_classes_i;
@@ -306,7 +303,7 @@
val axioms =
map (apsnd (Term.compress_term o Logic.varify) o prep_axm sign) raw_axms';
val ext_sg = Sign.add_space (axiomK, map fst axioms);
- in ext_theory thy ext_sg I axioms [] end;
+ in ext_theory thy ext_sg axioms [] end;
val add_axioms = ext_axms read_axm;
val add_axioms_i = ext_axms cert_axm;
@@ -318,7 +315,7 @@
let
val name = Sign.full_name sign raw_name;
val ext_sg = Sign.add_space (oracleK, [name]);
- in ext_theory thy ext_sg I [] [(name, (oracle, stamp ()))] end;
+ in ext_theory thy ext_sg [] [(name, (oracle, stamp ()))] end;
@@ -421,17 +418,11 @@
end))))
end
-fun check_defn sg overloaded final_consts ((deps, axms), def as (name, tm)) =
+fun check_defn sg overloaded ((deps, axms), def as (name, tm)) =
let
val name = Sign.full_name sg name
- fun is_final (c, ty) =
- case Symtab.lookup(final_consts,c) of
- SOME [] => true
- | SOME tys => exists (curry (Sign.typ_instance sg) ty) tys
- | NONE => false;
-
fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
@@ -446,9 +437,9 @@
handle TERM (msg, _) => err_in_defn sg name msg;
fun decl deps c =
- (case Sign.const_type sg c of
- SOME T => (Defs.declare deps c T handle _ => deps, T)
- | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
+ (case Sign.const_type sg c of
+ SOME T => (Defs.declare deps (c, T) handle _ => deps, T)
+ | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
val (deps, c_decl) = decl deps c
@@ -456,12 +447,6 @@
val deps = foldl (fn ((c, _), deps) => fst (decl deps c)) deps body
in
- if is_final c_ty then
- err_in_defn sg name (Pretty.string_of (Pretty.block
- ([Pretty.str "The constant",Pretty.brk 1] @
- pretty_const c_ty @
- [Pretty.brk 1,Pretty.str "has been declared final"])))
- else
(case overloading sg c_decl ty of
Useless =>
err_in_defn sg name (Pretty.string_of (Pretty.chunks
@@ -469,19 +454,24 @@
"imposes additional sort constraints on the declared type of the constant"]))
| ov =>
let
- val deps' = Defs.define deps c ty name body
+ val deps' = Defs.define deps c_ty name body
handle Defs.DEFS s => err_in_defn sg name ("DEFS: "^s)
| Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg (false, s))
| Defs.INFINITE_CHAIN s => err_in_defn sg name (cycle_msg sg (true, s))
| Defs.CLASH (_, def1, def2) => err_in_defn sg name (
- "clashing definitions "^ quote def1 ^" and "^ quote def2)
- in
- ((if ov = Plain andalso not overloaded then
- warning (Pretty.string_of (Pretty.chunks
- [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " ^ quote name ^ ")")]))
- else
- ()); (deps', def::axms))
- end)
+ "clashing definitions "^ quote def1 ^" and "^ quote def2)
+ | Defs.FINAL cfinal =>
+ err_in_defn sg name (Pretty.string_of (Pretty.block
+ ([Pretty.str "The constant",Pretty.brk 1] @
+ pretty_const cfinal @
+ [Pretty.brk 1,Pretty.str "has been declared final"])))
+ in
+ ((if ov = Plain andalso not overloaded then
+ warning (Pretty.string_of (Pretty.chunks
+ [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " ^ quote name ^ ")")]))
+ else
+ ()); (deps', def::axms))
+ end)
end;
@@ -489,13 +479,13 @@
fun ext_defns prep_axm overloaded raw_axms thy =
let
- val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
+ val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
val all_axioms = List.concat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors));
val axms = map (prep_axm sign) raw_axms;
- val (const_deps', _) = Library.foldl (check_defn sign overloaded final_consts) ((const_deps, all_axioms), axms);
+ val (const_deps', _) = Library.foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms);
in
- make_theory sign const_deps' final_consts axioms oracles parents ancestors
+ make_theory sign const_deps' axioms oracles parents ancestors
|> add_axioms_i axms
end;
@@ -507,39 +497,29 @@
fun ext_finals prep_term overloaded raw_terms thy =
let
- val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
- fun mk_final (finals,tm) =
- let
- fun err msg = raise TERM(msg,[tm]);
- val (c,ty) = dest_Const tm
- handle TERM _ => err "Can only make constants final";
- val c_decl =
- (case Sign.const_type sign c of SOME T => T
- | NONE => err ("Undeclared constant " ^ quote c));
- val simple =
- case overloading sign c_decl ty of
- NoOverloading => true
- | Useless => err "Sort restrictions too strong"
- | Plain => if overloaded then false
- else err "Type is more general than declared";
- val typ_instance = Sign.typ_instance sign;
- in
- if simple then
- (case Symtab.lookup(finals,c) of
- SOME [] => err "Constant already final"
- | _ => Symtab.update((c,[]),finals))
- else
- (case Symtab.lookup(finals,c) of
- SOME [] => err "Constant already completely final"
- | SOME tys => if exists (curry typ_instance ty) tys
- then err "Instance of constant is already final"
- else Symtab.update((c,ty::gen_rem typ_instance (tys,ty)),finals)
- | NONE => Symtab.update((c,[ty]),finals))
- end;
+ val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
+ fun mk_final (tm, finals) =
+ let
+ fun err msg = raise TERM(msg,[tm])
+ val (c,ty) = dest_Const tm
+ handle TERM _ => err "Can only make constants final"
+ val c_decl =
+ (case Sign.const_type sign c of
+ SOME T => T
+ | NONE => err ("Undeclared constant " ^ quote c))
+ val _ =
+ case overloading sign c_decl ty of
+ NoOverloading => ()
+ | Useless => err "Sort restrictions too strong"
+ | Plain => (if overloaded then () else warning "Type is more general than declared")
+ val finals = Defs.declare finals (c, c_decl) handle _ => finals
+ in
+ Defs.finalize finals (c,ty)
+ end
val consts = map (prep_term sign) raw_terms;
- val final_consts' = Library.foldl mk_final (final_consts,consts);
+ val const_deps' = foldl mk_final const_deps consts;
in
- make_theory sign const_deps final_consts' axioms oracles parents ancestors
+ make_theory sign const_deps' axioms oracles parents ancestors
end;
local
@@ -585,9 +565,6 @@
handle Defs.CIRCULAR namess => error (cycle_msg sign' (false, namess))
| Defs.INFINITE_CHAIN namess => error (cycle_msg sign' (true, namess))
- val final_constss = map (#final_consts o rep_theory) thys;
- val final_consts' =
- Library.foldl (Symtab.join (merge_final sign')) (hd final_constss, tl final_constss);
val axioms' = Symtab.empty;
fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
@@ -600,7 +577,7 @@
val ancestors' =
gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
in
- make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
+ make_theory sign' deps' axioms' oracles' parents' ancestors'
end;