# HG changeset patch # User obua # Date 1117560761 -7200 # Node ID 2c3565b74b7aaba3b59c8e11c320f38f87ceb6ec # Parent 1764cc98bafd2e9e44e1e247def545c8bab90795 Removed final_consts from theory data. Now const_deps deals with final constants. diff -r 1764cc98bafd -r 2c3565b74b7a src/Pure/defs.ML --- 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; diff -r 1764cc98bafd -r 2c3565b74b7a src/Pure/display.ML --- a/src/Pure/display.ML Tue May 31 17:52:10 2005 +0200 +++ b/src/Pure/display.ML Tue May 31 19:32:41 2005 +0200 @@ -223,7 +223,7 @@ fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t]; - val {sign = _, const_deps = _, final_consts, axioms, oracles, + val {sign = _, const_deps = const_deps, axioms, oracles, parents = _, ancestors = _} = Theory.rep_theory thy; val {self = _, tsig, consts, naming, spaces, data} = Sign.rep_sg sg; val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig; @@ -232,7 +232,7 @@ val tdecls = Symtab.dest types |> map (fn (t, (d, _)) => (Sign.extern sg Sign.typeK t, (t, d))) |> Library.sort_wrt #1 |> map #2; val cnsts = Sign.extern_table sg Sign.constK consts; - val finals = Sign.extern_table sg Sign.constK final_consts; + val finals = Sign.extern_table sg Sign.constK (Defs.finals const_deps) val axms = Sign.extern_table sg Theory.axiomK axioms; val oras = Sign.extern_table sg Theory.oracleK oracles; in diff -r 1764cc98bafd -r 2c3565b74b7a src/Pure/theory.ML --- 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;