Removed final_consts from theory data. Now const_deps deals with final
authorobua
Tue May 31 19:32:41 2005 +0200 (2005-05-31)
changeset 161582c3565b74b7a
parent 16157 1764cc98bafd
child 16159 99c3168438ea
Removed final_consts from theory data. Now const_deps deals with final
constants.
src/Pure/defs.ML
src/Pure/display.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/defs.ML	Tue May 31 17:52:10 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Tue May 31 19:32:41 2005 +0200
     1.3 @@ -14,11 +14,17 @@
     1.4      exception DEFS of string
     1.5      exception CIRCULAR of (typ * string * string) list
     1.6      exception INFINITE_CHAIN of (typ * string * string) list 
     1.7 +    exception FINAL of string * typ
     1.8      exception CLASH of string * string * string
     1.9      
    1.10      val empty : graph
    1.11 -    val declare : graph -> string -> typ -> graph  (* exception DEFS *)
    1.12 -    val define : graph -> string -> typ -> string -> (string * typ) list -> graph (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH *)
    1.13 +    val declare : graph -> string * typ -> graph  (* exception DEFS *)
    1.14 +    val define : graph -> string * typ -> string -> (string * typ) list -> graph 
    1.15 +      (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)
    1.16 +    
    1.17 +    val finalize : graph -> string * typ -> graph (* exception DEFS *)
    1.18 +
    1.19 +    val finals : graph -> (typ list) Symtab.table
    1.20  
    1.21      (* the first argument should be the smaller graph *)
    1.22      val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
    1.23 @@ -37,33 +43,26 @@
    1.24       * defnode Symtab.table  (* a table of defnodes, each corresponding to 1 definition of the constant for a particular type, 
    1.25                               indexed by axiom name *)
    1.26       * backref Symtab.table (* a table of all back references to this node, indexed by node name *)
    1.27 +     * typ list (* a list of all finalized types *)
    1.28       
    1.29  and defnode = Defnode of
    1.30         typ  (* type of the constant in this particular definition *)
    1.31       * ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *)
    1.32  
    1.33  and backref = Backref of
    1.34 -       noderef  (* a reference to the node that has defnodes which reference a certain node A *)
    1.35 +       noderef  (* the name of the node that has defnodes which reference a certain node A *)
    1.36       * (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *)
    1.37  
    1.38  fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
    1.39 -fun get_nodename (Node (n, _, _ ,_)) = n
    1.40 -fun get_nodedefs (Node (_, _, defs, _)) = defs
    1.41 -fun get_defnode (Node (_, _, defs, _)) defname = Symtab.lookup (defs, defname)
    1.42 +fun get_nodename (Node (n, _, _ ,_, _)) = n
    1.43 +fun get_nodedefs (Node (_, _, defs, _, _)) = defs
    1.44 +fun get_defnode (Node (_, _, defs, _, _)) defname = Symtab.lookup (defs, defname)
    1.45  fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
    1.46 -fun get_nodename (Node (n, _, _ ,_)) = n
    1.47 -
    1.48 +fun get_nodename (Node (n, _, _ , _, _)) = n
    1.49  
    1.50 -(*fun t2list t = rev (Symtab.foldl (fn (l, d) => d::l) ([], t))
    1.51 -fun tmap f t = map (fn (a,b) => (a, f b)) t
    1.52 -fun defnode2data (Defnode (typ, table)) = ("Defnode", typ, t2list table)
    1.53 -fun backref2data (Backref (noderef, table)) = ("Backref", noderef, map fst (t2list table))
    1.54 -fun node2data (Node (s, t, defs, backs)) = ("Node", ("nodename", s), ("nodetyp", t), 
    1.55 -					    ("defs", tmap defnode2data (t2list defs)), ("backs", tmap backref2data (t2list backs)))
    1.56 -fun graph2data g = ("Graph", tmap node2data (t2list g))
    1.57 -*)
    1.58 -
    1.59 -datatype graphaction = Declare of string * typ | Define of string * typ * string * (string * typ) list
    1.60 +datatype graphaction = Declare of string * typ 
    1.61 +		     | Define of string * typ * string * (string * typ) list
    1.62 +		     | Finalize of string * typ
    1.63  
    1.64  type graph = (graphaction list) * (node Symtab.table)
    1.65  
    1.66 @@ -73,13 +72,14 @@
    1.67  exception CIRCULAR of (typ * string * string) list;
    1.68  exception INFINITE_CHAIN of (typ * string * string) list;
    1.69  exception CLASH of string * string * string;
    1.70 +exception FINAL of string * typ;
    1.71  
    1.72  fun def_err s = raise (DEFS s)
    1.73  
    1.74 -fun declare (actions, g) name ty =
    1.75 -    ((Declare (name, ty))::actions, 
    1.76 -     Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty)), g))
    1.77 -    handle Symtab.DUP _ => def_err "declare: constant is already defined"
    1.78 +fun declare (actions, g) (cty as (name, ty)) =
    1.79 +    ((Declare cty)::actions, 
    1.80 +     Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty, [])), g))
    1.81 +    handle Symtab.DUP _ => def_err "constant is already declared"
    1.82  
    1.83  fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;  
    1.84  
    1.85 @@ -216,7 +216,7 @@
    1.86  	Symtab.foldl g (a, def_edges)
    1.87      end	
    1.88  
    1.89 -fun define (actions, graph) name ty axname body =
    1.90 +fun define (actions, graph) (name, ty) axname body =
    1.91      let
    1.92  	val ty = checkT ty
    1.93  	val body = map (fn (n,t) => (n, checkT t)) body		 
    1.94 @@ -224,15 +224,22 @@
    1.95  	val mainnode  = (case Symtab.lookup (graph, mainref) of 
    1.96  			     NONE => def_err ("constant "^(quote mainref)^" is not declared")
    1.97  			   | SOME n => n)
    1.98 -	val (Node (n, gty, defs, backs)) = mainnode
    1.99 +	val (Node (n, gty, defs, backs, finals)) = mainnode
   1.100  	val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
   1.101  	fun check_def (s, Defnode (ty', _)) = 
   1.102  	    (if can_be_unified_r ty ty' then 
   1.103  		 raise (CLASH (mainref, axname, s))
   1.104  	     else if s = axname then
   1.105  	         def_err "name of axiom is already used for another definition of this constant"
   1.106 -	     else true)
   1.107 +	     else true)	
   1.108  	val _ = forall_table check_def defs		
   1.109 +	fun check_final finalty = 
   1.110 +	    (if can_be_unified_r finalty ty then
   1.111 +		 raise (FINAL (mainref, finalty))
   1.112 +	     else
   1.113 +		 true)
   1.114 +	val _ = forall check_final finals
   1.115 +	
   1.116  	(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
   1.117  
   1.118  	(* body contains the constants that this constant definition depends on. For each element of body,
   1.119 @@ -244,7 +251,7 @@
   1.120  		    (case Symtab.lookup (graph, bodyn) of 
   1.121  			 NONE => def_err "body of constant definition references undeclared constant"
   1.122  		       | SOME x => x)
   1.123 -		val (Node (_, general_btyp, bdefs, bbacks)) = bnode
   1.124 +		val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode
   1.125  	    in
   1.126  		case unify_r 0 bodyty general_btyp of
   1.127  		    NONE => NONE
   1.128 @@ -260,13 +267,13 @@
   1.129  			      (case unify_r 0 bodyty def_ty of
   1.130  				   NONE => (swallowed, l)
   1.131  				 | SOME (maxidx, sigma1, sigma2) => 
   1.132 -				   (is_instance bodyty def_ty,
   1.133 +				   (is_instance_r bodyty def_ty,
   1.134  				    merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
   1.135            	      val (swallowed, edges) = Symtab.foldl make_edges ((false, []), bdefs)
   1.136  		    in
   1.137 -			if swallowed then 
   1.138 +			if swallowed orelse (exists (is_instance_r bodyty) bfinals) then 
   1.139  			    (bodyn, edges)
   1.140 -			else
   1.141 +			else 
   1.142  			    (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
   1.143  		    end)
   1.144  	    end 
   1.145 @@ -339,8 +346,8 @@
   1.146  	
   1.147  	fun install_backref graph noderef pointingnoderef pointingdefname = 
   1.148  	    let
   1.149 -		val (Node (pname, _, _, _)) = getnode graph pointingnoderef
   1.150 -		val (Node (name, ty, defs, backs)) = getnode graph noderef
   1.151 +		val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
   1.152 +		val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
   1.153  	    in
   1.154  		case Symtab.lookup (backs, pname) of
   1.155  		    NONE => 
   1.156 @@ -348,14 +355,14 @@
   1.157  			val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
   1.158  			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   1.159  		    in
   1.160 -			Symtab.update ((name, Node (name, ty, defs, backs)), graph) 			
   1.161 +			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 			
   1.162  		    end
   1.163  		  | SOME (Backref (pointingnoderef, defnames)) =>
   1.164  		    let
   1.165  			val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
   1.166  			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   1.167  		    in
   1.168 -			Symtab.update ((name, Node (name, ty, defs, backs)), graph)
   1.169 +			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
   1.170  		    end
   1.171  		    handle Symtab.DUP _ => graph
   1.172  	    end
   1.173 @@ -368,8 +375,9 @@
   1.174  
   1.175          val graph = Symtab.foldl install_backrefs (graph, edges)
   1.176  
   1.177 -        val (Node (_, _, _, backs)) = getnode graph mainref
   1.178 -	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new ((axname, thisDefnode), defs), backs)), graph)
   1.179 +        val (Node (_, _, _, backs, _)) = getnode graph mainref
   1.180 +	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
   1.181 +          ((axname, thisDefnode), defs), backs, finals)), graph)
   1.182  		    
   1.183  	(* Now we have to check all backreferences to this node and inform them about the new defnode. 
   1.184  	   In this section we also check for circularity. *)
   1.185 @@ -420,7 +428,7 @@
   1.186  			    in
   1.187  				(defnames, (defname, none_edges, this_edges)::newedges)
   1.188  			    end			    
   1.189 -			  | _ => def_err "update_defs, internal error, corrupt backrefs"
   1.190 +			  | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
   1.191  		    end
   1.192  		    
   1.193  		val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
   1.194 @@ -440,13 +448,14 @@
   1.195  						 
   1.196  	(* If a Circular exception is thrown then we never reach this point. *)
   1.197          (* Ok, the definition is consistent, let's update this node. *)
   1.198 -	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update ((axname, thisDefnode), defs), backs)), graph)
   1.199 +	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
   1.200 +	  ((axname, thisDefnode), defs), backs, finals)), graph)
   1.201  
   1.202          (* Furthermore, update all the other nodes that backreference this node. *)
   1.203          fun final_update_backrefs graph noderef defname none_edges this_edges =
   1.204  	    let
   1.205  		val node = getnode graph noderef
   1.206 -		val (Node (nodename, nodety, defs, backs)) = node
   1.207 +		val (Node (nodename, nodety, defs, backs, finals)) = node
   1.208  		val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
   1.209  		val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
   1.210  
   1.211 @@ -467,7 +476,7 @@
   1.212  		val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
   1.213  		val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
   1.214  	    in
   1.215 -		Symtab.update ((nodename, Node (nodename, nodety, defs', backs)), graph)
   1.216 +		Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
   1.217  	    end
   1.218  
   1.219  	val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
   1.220 @@ -477,18 +486,78 @@
   1.221  	((Define (name, ty, axname, body))::actions, graph)	   
   1.222      end 
   1.223  
   1.224 +    fun finalize' ((c, ty), graph) = 
   1.225 +      case Symtab.lookup (graph, c) of 
   1.226 +	  NONE => def_err ("finalize: constant "^(quote c)^" is not declared")
   1.227 +	| SOME (Node (noderef, nodety, defs, backs, finals)) =>
   1.228 +	  let 
   1.229 +	      val nodety = checkT nodety 
   1.230 +	  in
   1.231 +	      if (not (is_instance_r ty nodety)) then
   1.232 +		  def_err ("finalize: only type instances of the declared constant "^(quote c)^" can be finalized")
   1.233 +	      else if exists (is_instance_r ty) finals then
   1.234 +		  graph
   1.235 +	      else 
   1.236 +	      let
   1.237 +	          val finals = ty :: finals
   1.238 +		  val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
   1.239 +		  fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
   1.240 +		  let
   1.241 +		      fun update_backdef ((graph, defnames), (backdefname, _)) = 
   1.242 +	              let 
   1.243 +			  val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
   1.244 +			  val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)						      
   1.245 +			  val (defnames', all_edges') = 
   1.246 +			      case Symtab.lookup (all_edges, noderef) of
   1.247 +				  NONE => sys_error "finalize: corrupt backref"
   1.248 +				| SOME (_, (NONE, edges)::rest) =>
   1.249 +				  let
   1.250 +				      val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
   1.251 +				  in
   1.252 +				      if edges' = [] then 
   1.253 +					  (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
   1.254 +				      else
   1.255 +					  (Symtab.update ((backdefname, ()), defnames), 
   1.256 +					   Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
   1.257 +				  end
   1.258 +			  val defnode' = Defnode (def_ty, all_edges')
   1.259 +			  val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
   1.260 +					   backbacks, backfinals)
   1.261 +		      in
   1.262 +			  (Symtab.update ((backrefname, backnode'), graph), defnames')			  			  
   1.263 +		      end
   1.264 +	  
   1.265 +		      val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   1.266 +		  in
   1.267 +		      (graph', if Symtab.is_empty defnames' then backs 
   1.268 +			       else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
   1.269 +		  end
   1.270 +		  val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   1.271 +		  val Node (_, _, defs, _, _) = getnode graph' noderef
   1.272 +	      in
   1.273 +		  Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph')
   1.274 +	      end
   1.275 +	  end
   1.276 +	   
   1.277 +    fun finalize (history, graph) c_ty = ((Finalize c_ty)::history, finalize' (c_ty, graph))
   1.278      
   1.279 -    fun merge' (Declare (name, ty), g) = (declare g name ty handle _ => g)
   1.280 +    fun merge' (Declare cty, g) = (declare g cty handle _ => g)
   1.281        | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
   1.282  	(case Symtab.lookup (graph, name) of
   1.283 -	     NONE => define g name ty axname body
   1.284 -	   | SOME (Node (_, _, defs, _)) => 
   1.285 +	     NONE => define g (name, ty) axname body
   1.286 +	   | SOME (Node (_, _, defs, _, _)) => 
   1.287  	     (case Symtab.lookup (defs, axname) of
   1.288 -		  NONE => define g name ty axname body
   1.289 +		  NONE => define g (name, ty) axname body
   1.290  		| SOME _ => g))
   1.291 +      | merge' (Finalize finals, g) = (finalize g finals handle _ => g)
   1.292  	
   1.293      fun merge (actions, _) g = foldr merge' g actions
   1.294  
   1.295 +    fun finals (history, graph) = 
   1.296 +	Symtab.foldl 
   1.297 +	    (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
   1.298 +	    (Symtab.empty, graph)
   1.299 +
   1.300  end;
   1.301  		
   1.302  
     2.1 --- a/src/Pure/display.ML	Tue May 31 17:52:10 2005 +0200
     2.2 +++ b/src/Pure/display.ML	Tue May 31 19:32:41 2005 +0200
     2.3 @@ -223,7 +223,7 @@
     2.4      fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
     2.5  
     2.6  
     2.7 -    val {sign = _, const_deps = _, final_consts, axioms, oracles,
     2.8 +    val {sign = _, const_deps = const_deps,  axioms, oracles,
     2.9        parents = _, ancestors = _} = Theory.rep_theory thy;
    2.10      val {self = _, tsig, consts, naming, spaces, data} = Sign.rep_sg sg;
    2.11      val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
    2.12 @@ -232,7 +232,7 @@
    2.13      val tdecls = Symtab.dest types |> map (fn (t, (d, _)) =>
    2.14        (Sign.extern sg Sign.typeK t, (t, d))) |> Library.sort_wrt #1 |> map #2;
    2.15      val cnsts = Sign.extern_table sg Sign.constK consts;
    2.16 -    val finals = Sign.extern_table sg Sign.constK final_consts;
    2.17 +    val finals = Sign.extern_table sg Sign.constK (Defs.finals const_deps)
    2.18      val axms = Sign.extern_table sg Theory.axiomK axioms;
    2.19      val oras = Sign.extern_table sg Theory.oracleK oracles;
    2.20    in
     3.1 --- a/src/Pure/theory.ML	Tue May 31 17:52:10 2005 +0200
     3.2 +++ b/src/Pure/theory.ML	Tue May 31 19:32:41 2005 +0200
     3.3 @@ -4,7 +4,6 @@
     3.4  
     3.5  The abstract type "theory" of theories.
     3.6  *)
     3.7 -
     3.8  signature BASIC_THEORY =
     3.9  sig
    3.10    type theory
    3.11 @@ -12,7 +11,6 @@
    3.12    val rep_theory: theory ->
    3.13      {sign: Sign.sg,
    3.14        const_deps: Defs.graph,
    3.15 -      final_consts: typ list Symtab.table,
    3.16        axioms: term Symtab.table,
    3.17        oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    3.18        parents: theory list,
    3.19 @@ -131,14 +129,13 @@
    3.20    Theory of {
    3.21      sign: Sign.sg,
    3.22      const_deps: Defs.graph,
    3.23 -    final_consts: typ list Symtab.table,
    3.24      axioms: term Symtab.table,
    3.25      oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    3.26      parents: theory list,
    3.27      ancestors: theory list};
    3.28  
    3.29 -fun make_theory sign const_deps final_consts axioms oracles parents ancestors =
    3.30 -  Theory {sign = sign, const_deps = const_deps, final_consts = final_consts, axioms = axioms,
    3.31 +fun make_theory sign const_deps axioms oracles parents ancestors =
    3.32 +  Theory {sign = sign, const_deps = const_deps, axioms = axioms,
    3.33      oracles = oracles,  parents = parents, ancestors = ancestors};
    3.34  
    3.35  fun rep_theory (Theory args) = args;
    3.36 @@ -167,7 +164,7 @@
    3.37  
    3.38  (*partial Pure theory*)
    3.39  val pre_pure =
    3.40 -  make_theory Sign.pre_pure Defs.empty Symtab.empty Symtab.empty Symtab.empty [] [];
    3.41 +  make_theory Sign.pre_pure Defs.empty Symtab.empty Symtab.empty [] [];
    3.42  
    3.43  
    3.44  
    3.45 @@ -186,9 +183,9 @@
    3.46  fun err_dup_oras names =
    3.47    error ("Duplicate oracles: " ^ commas_quote names);
    3.48  
    3.49 -fun ext_theory thy ext_sg ext_deps new_axms new_oras =
    3.50 +fun ext_theory thy ext_sg new_axms new_oras =
    3.51    let
    3.52 -    val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
    3.53 +    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
    3.54      val draft = Sign.is_draft sign;
    3.55      val axioms' =
    3.56        Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
    3.57 @@ -199,13 +196,13 @@
    3.58      val (parents', ancestors') =
    3.59        if draft then (parents, ancestors) else ([thy], thy :: ancestors);
    3.60    in
    3.61 -    make_theory (ext_sg sign) (ext_deps const_deps) final_consts axioms' oracles' parents' ancestors'
    3.62 +    make_theory (ext_sg sign) const_deps axioms' oracles' parents' ancestors'
    3.63    end;
    3.64  
    3.65  
    3.66  (* extend signature of a theory *)
    3.67  
    3.68 -fun ext_sign ext_sg args thy = ext_theory thy (ext_sg args) I [] [];
    3.69 +fun ext_sign ext_sg args thy = ext_theory thy (ext_sg args) [] [];
    3.70  
    3.71  val add_classes            = ext_sign Sign.add_classes;
    3.72  val add_classes_i          = ext_sign Sign.add_classes_i;
    3.73 @@ -306,7 +303,7 @@
    3.74      val axioms =
    3.75        map (apsnd (Term.compress_term o Logic.varify) o prep_axm sign) raw_axms';
    3.76      val ext_sg = Sign.add_space (axiomK, map fst axioms);
    3.77 -  in ext_theory thy ext_sg I axioms [] end;
    3.78 +  in ext_theory thy ext_sg axioms [] end;
    3.79  
    3.80  val add_axioms = ext_axms read_axm;
    3.81  val add_axioms_i = ext_axms cert_axm;
    3.82 @@ -318,7 +315,7 @@
    3.83    let
    3.84      val name = Sign.full_name sign raw_name;
    3.85      val ext_sg = Sign.add_space (oracleK, [name]);
    3.86 -  in ext_theory thy ext_sg I [] [(name, (oracle, stamp ()))] end;
    3.87 +  in ext_theory thy ext_sg [] [(name, (oracle, stamp ()))] end;
    3.88  
    3.89  
    3.90  
    3.91 @@ -421,17 +418,11 @@
    3.92  	end))))
    3.93    end
    3.94  
    3.95 -fun check_defn sg overloaded final_consts ((deps, axms), def as (name, tm)) =
    3.96 +fun check_defn sg overloaded ((deps, axms), def as (name, tm)) =
    3.97    let
    3.98      
    3.99      val name = Sign.full_name sg name
   3.100        
   3.101 -    fun is_final (c, ty) =
   3.102 -      case Symtab.lookup(final_consts,c) of
   3.103 -        SOME [] => true
   3.104 -      | SOME tys => exists (curry (Sign.typ_instance sg) ty) tys
   3.105 -      | NONE => false;
   3.106 -
   3.107      fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   3.108        Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
   3.109  
   3.110 @@ -446,9 +437,9 @@
   3.111        handle TERM (msg, _) => err_in_defn sg name msg;
   3.112  
   3.113      fun decl deps c = 
   3.114 -        (case Sign.const_type sg c of 
   3.115 -             SOME T => (Defs.declare deps c T handle _ => deps, T)
   3.116 -           | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
   3.117 +	(case Sign.const_type sg c of 
   3.118 +	     SOME T => (Defs.declare deps (c, T) handle _ => deps, T)
   3.119 +	   | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
   3.120  
   3.121      val (deps, c_decl) = decl deps c
   3.122  
   3.123 @@ -456,12 +447,6 @@
   3.124      val deps = foldl (fn ((c, _), deps) => fst (decl deps c)) deps body
   3.125  
   3.126    in
   3.127 -    if is_final c_ty then
   3.128 -      err_in_defn sg name (Pretty.string_of (Pretty.block
   3.129 -        ([Pretty.str "The constant",Pretty.brk 1] @
   3.130 -         pretty_const c_ty @
   3.131 -         [Pretty.brk 1,Pretty.str "has been declared final"])))
   3.132 -    else
   3.133        (case overloading sg c_decl ty of
   3.134           Useless =>
   3.135             err_in_defn sg name (Pretty.string_of (Pretty.chunks
   3.136 @@ -469,19 +454,24 @@
   3.137                "imposes additional sort constraints on the declared type of the constant"]))   
   3.138         | ov =>
   3.139  	 let 
   3.140 -	     val deps' = Defs.define deps c ty name body
   3.141 +	     val deps' = Defs.define deps c_ty name body
   3.142  		 handle Defs.DEFS s => err_in_defn sg name ("DEFS: "^s) 
   3.143  		      | Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg (false, s))
   3.144                        | Defs.INFINITE_CHAIN s => err_in_defn sg name (cycle_msg sg (true, s)) 
   3.145                        | Defs.CLASH (_, def1, def2) => err_in_defn sg name (
   3.146 -                          "clashing definitions "^ quote def1 ^" and "^ quote def2)
   3.147 -         in
   3.148 -             ((if ov = Plain andalso not overloaded then
   3.149 -                   warning (Pretty.string_of (Pretty.chunks
   3.150 -                     [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " ^ quote name ^ ")")]))
   3.151 -               else
   3.152 -                   ()); (deps', def::axms))
   3.153 -         end)
   3.154 +			  "clashing definitions "^ quote def1 ^" and "^ quote def2)
   3.155 +		      | Defs.FINAL cfinal =>
   3.156 +			err_in_defn sg name (Pretty.string_of (Pretty.block
   3.157 +			  ([Pretty.str "The constant",Pretty.brk 1] @
   3.158 +			   pretty_const cfinal @
   3.159 +			   [Pretty.brk 1,Pretty.str "has been declared final"]))) 
   3.160 +	 in
   3.161 +	     ((if ov = Plain andalso not overloaded then
   3.162 +		   warning (Pretty.string_of (Pretty.chunks
   3.163 +		     [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " ^ quote name ^ ")")]))
   3.164 +	       else
   3.165 +		   ()); (deps', def::axms))
   3.166 +	 end)
   3.167    end;
   3.168  
   3.169  
   3.170 @@ -489,13 +479,13 @@
   3.171  
   3.172  fun ext_defns prep_axm overloaded raw_axms thy =
   3.173    let
   3.174 -    val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
   3.175 +    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
   3.176      val all_axioms = List.concat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors));
   3.177  
   3.178      val axms = map (prep_axm sign) raw_axms;
   3.179 -    val (const_deps', _) = Library.foldl (check_defn sign overloaded final_consts) ((const_deps, all_axioms), axms);
   3.180 +    val (const_deps', _) = Library.foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms);
   3.181    in
   3.182 -    make_theory sign const_deps' final_consts axioms oracles parents ancestors
   3.183 +    make_theory sign const_deps' axioms oracles parents ancestors
   3.184      |> add_axioms_i axms
   3.185    end;
   3.186  
   3.187 @@ -507,39 +497,29 @@
   3.188  
   3.189  fun ext_finals prep_term overloaded raw_terms thy =
   3.190    let
   3.191 -    val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
   3.192 -    fun mk_final (finals,tm) =
   3.193 -      let
   3.194 -        fun err msg = raise TERM(msg,[tm]);
   3.195 -        val (c,ty) = dest_Const tm
   3.196 -          handle TERM _ => err "Can only make constants final";
   3.197 -        val c_decl =
   3.198 -          (case Sign.const_type sign c of SOME T => T
   3.199 -          | NONE => err ("Undeclared constant " ^ quote c));
   3.200 -        val simple =
   3.201 -          case overloading sign c_decl ty of
   3.202 -            NoOverloading => true
   3.203 -          | Useless => err "Sort restrictions too strong"
   3.204 -          | Plain => if overloaded then false
   3.205 -                     else err "Type is more general than declared";
   3.206 -        val typ_instance = Sign.typ_instance sign;
   3.207 -      in
   3.208 -        if simple then
   3.209 -          (case Symtab.lookup(finals,c) of
   3.210 -            SOME [] => err "Constant already final"
   3.211 -          | _ => Symtab.update((c,[]),finals))
   3.212 -        else
   3.213 -          (case Symtab.lookup(finals,c) of
   3.214 -            SOME [] => err "Constant already completely final"
   3.215 -          | SOME tys => if exists (curry typ_instance ty) tys
   3.216 -                        then err "Instance of constant is already final"
   3.217 -                        else Symtab.update((c,ty::gen_rem typ_instance (tys,ty)),finals)
   3.218 -          | NONE => Symtab.update((c,[ty]),finals))
   3.219 -      end;
   3.220 +    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
   3.221 +    fun mk_final (tm, finals) =
   3.222 +	let
   3.223 +            fun err msg = raise TERM(msg,[tm])
   3.224 +            val (c,ty) = dest_Const tm
   3.225 +		handle TERM _ => err "Can only make constants final"
   3.226 +            val c_decl =
   3.227 +		(case Sign.const_type sign c of 
   3.228 +		     SOME T => T
   3.229 +		   | NONE => err ("Undeclared constant " ^ quote c))
   3.230 +	    val _ =
   3.231 +		case overloading sign c_decl ty of
   3.232 +		    NoOverloading => ()
   3.233 +		  | Useless => err "Sort restrictions too strong"
   3.234 +		  | Plain => (if overloaded then () else warning "Type is more general than declared")
   3.235 +	    val finals = Defs.declare finals (c, c_decl) handle _ => finals
   3.236 +	in
   3.237 +	    Defs.finalize finals (c,ty)
   3.238 +	end
   3.239      val consts = map (prep_term sign) raw_terms;
   3.240 -    val final_consts' = Library.foldl mk_final (final_consts,consts);
   3.241 +    val const_deps' = foldl mk_final const_deps consts;
   3.242    in
   3.243 -    make_theory sign const_deps final_consts' axioms oracles parents ancestors
   3.244 +    make_theory sign const_deps' axioms oracles parents ancestors
   3.245    end;
   3.246  
   3.247  local
   3.248 @@ -585,9 +565,6 @@
   3.249        handle Defs.CIRCULAR namess => error (cycle_msg sign' (false, namess))
   3.250  	   | Defs.INFINITE_CHAIN namess => error (cycle_msg sign' (true, namess))
   3.251  
   3.252 -    val final_constss = map (#final_consts o rep_theory) thys;
   3.253 -    val final_consts' =
   3.254 -      Library.foldl (Symtab.join (merge_final sign')) (hd final_constss, tl final_constss);
   3.255      val axioms' = Symtab.empty;
   3.256  
   3.257      fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
   3.258 @@ -600,7 +577,7 @@
   3.259      val ancestors' =
   3.260        gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
   3.261    in
   3.262 -    make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
   3.263 +    make_theory sign' deps' axioms' oracles' parents' ancestors'
   3.264    end;
   3.265  
   3.266