src/Pure/defs.ML
changeset 16198 cfd070a2cc4d
parent 16177 1af9f5c69745
child 16308 636a1a84977a
     1.1 --- a/src/Pure/defs.ML	Thu Jun 02 18:29:58 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Fri Jun 03 01:08:07 2005 +0200
     1.3 @@ -9,25 +9,25 @@
     1.4  
     1.5  signature DEFS = sig
     1.6      
     1.7 -    type graph
     1.8 +  type graph
     1.9 +       
    1.10 +  exception DEFS of string
    1.11 +  exception CIRCULAR of (typ * string * string) list
    1.12 +  exception INFINITE_CHAIN of (typ * string * string) list 
    1.13 +  exception FINAL of string * typ
    1.14 +  exception CLASH of string * string * string
    1.15 +                     
    1.16 +  val empty : graph
    1.17 +  val declare : graph -> string * typ -> graph  (* exception DEFS *)
    1.18 +  val define : graph -> string * typ -> string -> (string * typ) list -> graph 
    1.19 +    (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)
    1.20 +                                                                         
    1.21 +  val finalize : graph -> string * typ -> graph (* exception DEFS *)
    1.22  
    1.23 -    exception DEFS of string
    1.24 -    exception CIRCULAR of (typ * string * string) list
    1.25 -    exception INFINITE_CHAIN of (typ * string * string) list 
    1.26 -    exception FINAL of string * typ
    1.27 -    exception CLASH of string * string * string
    1.28 -    
    1.29 -    val empty : graph
    1.30 -    val declare : graph -> string * typ -> graph  (* exception DEFS *)
    1.31 -    val define : graph -> string * typ -> string -> (string * typ) list -> graph 
    1.32 -      (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)
    1.33 -    
    1.34 -    val finalize : graph -> string * typ -> graph (* exception DEFS *)
    1.35 +  val finals : graph -> (typ list) Symtab.table
    1.36  
    1.37 -    val finals : graph -> (typ list) Symtab.table
    1.38 -
    1.39 -    (* the first argument should be the smaller graph *)
    1.40 -    val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
    1.41 +  (* the first argument should be the smaller graph *)
    1.42 +  val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
    1.43  
    1.44  end
    1.45  
    1.46 @@ -38,20 +38,20 @@
    1.47  type noderef = string
    1.48  
    1.49  datatype node = Node of
    1.50 -       string  (* name of constant *)
    1.51 -     * typ  (* most general type of constant *)
    1.52 -     * defnode Symtab.table  (* a table of defnodes, each corresponding to 1 definition of the constant for a particular type, 
    1.53 -                             indexed by axiom name *)
    1.54 -     * backref Symtab.table (* a table of all back references to this node, indexed by node name *)
    1.55 -     * typ list (* a list of all finalized types *)
    1.56 +         string  (* name of constant *)
    1.57 +         * typ  (* most general type of constant *)
    1.58 +         * defnode Symtab.table  (* a table of defnodes, each corresponding to 1 definition of the 
    1.59 +             constant for a particular type, indexed by axiom name *)
    1.60 +         * backref Symtab.table (* a table of all back references to this node, indexed by node name *)
    1.61 +         * typ list (* a list of all finalized types *)
    1.62       
    1.63 -and defnode = Defnode of
    1.64 -       typ  (* type of the constant in this particular definition *)
    1.65 -     * ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *)
    1.66 +     and defnode = Defnode of
    1.67 +         typ  (* type of the constant in this particular definition *)
    1.68 +         * ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *)
    1.69  
    1.70  and backref = Backref of
    1.71 -       noderef  (* the name of the node that has defnodes which reference a certain node A *)
    1.72 -     * (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *)
    1.73 +    noderef  (* the name of the node that has defnodes which reference a certain node A *)
    1.74 +    * (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *)
    1.75  
    1.76  fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
    1.77  fun get_nodename (Node (n, _, _ ,_, _)) = n
    1.78 @@ -65,7 +65,7 @@
    1.79  		     | Finalize of string * typ
    1.80  
    1.81  type graph = (graphaction list) * (node Symtab.table)
    1.82 -
    1.83 +             
    1.84  val empty = ([], Symtab.empty)
    1.85  
    1.86  exception DEFS of string;
    1.87 @@ -85,41 +85,41 @@
    1.88  
    1.89  fun subst_incr_tvar inc t =
    1.90      if (inc > 0) then 
    1.91 -	let
    1.92 -	    val tv = typ_tvars t
    1.93 -	    val t' = incr_tvar inc t
    1.94 -	    fun update_subst (((n,i), _), s) =
    1.95 -		Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
    1.96 -	in
    1.97 -	    (t',List.foldl update_subst Vartab.empty tv)
    1.98 -	end	
    1.99 +      let
   1.100 +	val tv = typ_tvars t
   1.101 +	val t' = incr_tvar inc t
   1.102 +	fun update_subst (((n,i), _), s) =
   1.103 +	    Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
   1.104 +      in
   1.105 +	(t',List.foldl update_subst Vartab.empty tv)
   1.106 +      end	
   1.107      else
   1.108 -	(t, Vartab.empty)
   1.109 +      (t, Vartab.empty)
   1.110  
   1.111  (* Rename tys2 so that tys2 and tys1 do not have any variables in common any more.
   1.112     As a result, return the renamed tys2' and the substitution that takes tys2 to tys2'. *)
   1.113  fun subst_rename max1 ty2 =
   1.114      let
   1.115 -        val max2 = (maxidx_of_typ ty2)
   1.116 -        val (ty2', s) = subst_incr_tvar (max1 + 1) ty2                
   1.117 +      val max2 = (maxidx_of_typ ty2)
   1.118 +      val (ty2', s) = subst_incr_tvar (max1 + 1) ty2                
   1.119      in
   1.120 -	(ty2', s, max1 + max2 + 1)
   1.121 +      (ty2', s, max1 + max2 + 1)
   1.122      end	       
   1.123 -
   1.124 +    
   1.125  fun subst s ty = Envir.norm_type s ty
   1.126 -
   1.127 +                 
   1.128  fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
   1.129 -
   1.130 +                              
   1.131  fun is_instance instance_ty general_ty =
   1.132      Type.typ_instance Type.empty_tsig (instance_ty, general_ty)
   1.133 -
   1.134 +    
   1.135  fun is_instance_r instance_ty general_ty =
   1.136      is_instance instance_ty (rename instance_ty general_ty)
   1.137 -
   1.138 +    
   1.139  fun unify ty1 ty2 = 
   1.140      SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2)))
   1.141      handle Type.TUNIFY => NONE
   1.142 -
   1.143 +                            
   1.144  (* 
   1.145     Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and so that they
   1.146     are different. All indices in ty1 and ty2 are supposed to be less than or equal to max.
   1.147 @@ -128,34 +128,34 @@
   1.148  *)
   1.149  fun unify_r max ty1 ty2 = 
   1.150      let
   1.151 -	val max =  Int.max(max, 0)
   1.152 -	val max1 = max (* >= maxidx_of_typ ty1 *)
   1.153 -	val max2 = max (* >= maxidx_of_typ ty2 *)
   1.154 -	val max = Int.max(max, Int.max (max1, max2))
   1.155 -        val (ty1, s1) = subst_incr_tvar (max+1) ty1
   1.156 -	val (ty2, s2) = subst_incr_tvar (max+max1+2) ty2
   1.157 -        val max = max+max1+max2+2	
   1.158 -	fun merge a b = Vartab.merge (fn _ => false) (a, b)
   1.159 +      val max =  Int.max(max, 0)
   1.160 +      val max1 = max (* >= maxidx_of_typ ty1 *)
   1.161 +      val max2 = max (* >= maxidx_of_typ ty2 *)
   1.162 +      val max = Int.max(max, Int.max (max1, max2))
   1.163 +      val (ty1, s1) = subst_incr_tvar (max+1) ty1
   1.164 +      val (ty2, s2) = subst_incr_tvar (max+max1+2) ty2
   1.165 +      val max = max+max1+max2+2	
   1.166 +      fun merge a b = Vartab.merge (fn _ => false) (a, b)
   1.167      in
   1.168 -	case unify ty1 ty2 of
   1.169 -	    NONE => NONE
   1.170 -	  | SOME s => SOME (max, merge s1 s, merge s2 s)
   1.171 +      case unify ty1 ty2 of
   1.172 +	NONE => NONE
   1.173 +      | SOME s => SOME (max, merge s1 s, merge s2 s)
   1.174      end
   1.175 -
   1.176 +    
   1.177  fun can_be_unified_r ty1 ty2 =
   1.178      let
   1.179 -	val ty2 = rename ty1 ty2
   1.180 +      val ty2 = rename ty1 ty2
   1.181      in
   1.182 -	case unify ty1 ty2 of
   1.183 -	    NONE => false
   1.184 -	  | _ => true
   1.185 +      case unify ty1 ty2 of
   1.186 +	NONE => false
   1.187 +      | _ => true
   1.188      end
   1.189 -
   1.190 +    
   1.191  fun can_be_unified ty1 ty2 =
   1.192      case unify ty1 ty2 of
   1.193 -	NONE => false
   1.194 -      | _ => true
   1.195 -
   1.196 +      NONE => false
   1.197 +    | _ => true
   1.198 +           
   1.199  fun checkT (Type (a, Ts)) = Type (a, map checkT Ts)
   1.200    | checkT (TVar ((a, 0), _)) = TVar ((a, 0), [])
   1.201    | checkT (TVar ((a, i), _)) = def_err "type is not clean"
   1.202 @@ -168,28 +168,28 @@
   1.203  
   1.204  fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
   1.205      let
   1.206 -	val t1 = u1 --> v1
   1.207 -	val t2 = u2 --> v2
   1.208 +      val t1 = u1 --> v1
   1.209 +      val t2 = u2 --> v2
   1.210      in
   1.211 -	if (is_instance_r t1 t2) then
   1.212 -	    (if is_instance_r t2 t1 then
   1.213 -		 SOME (int_ord (length history2, length history1))
   1.214 -	     else
   1.215 -		 SOME LESS)
   1.216 -	else if (is_instance_r t2 t1) then
   1.217 -	    SOME GREATER
   1.218 -	else
   1.219 -	    NONE
   1.220 +      if (is_instance_r t1 t2) then
   1.221 +	(if is_instance_r t2 t1 then
   1.222 +	   SOME (int_ord (length history2, length history1))
   1.223 +	 else
   1.224 +	   SOME LESS)
   1.225 +      else if (is_instance_r t2 t1) then
   1.226 +	SOME GREATER
   1.227 +      else
   1.228 +	NONE
   1.229      end
   1.230 -
   1.231 +    
   1.232  fun merge_edges_1 (x, []) = []
   1.233    | merge_edges_1 (x, (y::ys)) = 
   1.234      (case compare_edges x y of
   1.235 -	 SOME LESS => (y::ys)
   1.236 -       | SOME EQUAL => (y::ys)
   1.237 -       | SOME GREATER => merge_edges_1 (x, ys)
   1.238 -       | NONE => y::(merge_edges_1 (x, ys)))
   1.239 -
   1.240 +       SOME LESS => (y::ys)
   1.241 +     | SOME EQUAL => (y::ys)
   1.242 +     | SOME GREATER => merge_edges_1 (x, ys)
   1.243 +     | NONE => y::(merge_edges_1 (x, ys)))
   1.244 +    
   1.245  fun merge_edges xs ys = foldl merge_edges_1 xs ys
   1.246  
   1.247  fun pack_edges xs = merge_edges [] xs
   1.248 @@ -198,377 +198,381 @@
   1.249    | merge_labelled_edges es [] = es
   1.250    | merge_labelled_edges ((l1,e1)::es1) ((l2,e2)::es2) = 
   1.251      (case label_ord l1 l2 of
   1.252 -	 LESS => (l1, e1)::(merge_labelled_edges es1 ((l2, e2)::es2))
   1.253 -       | GREATER => (l2, e2)::(merge_labelled_edges ((l1, e1)::es1) es2)
   1.254 -       | EQUAL => (l1, merge_edges e1 e2)::(merge_labelled_edges es1 es2))
   1.255 -
   1.256 +       LESS => (l1, e1)::(merge_labelled_edges es1 ((l2, e2)::es2))
   1.257 +     | GREATER => (l2, e2)::(merge_labelled_edges ((l1, e1)::es1) es2)
   1.258 +     | EQUAL => (l1, merge_edges e1 e2)::(merge_labelled_edges es1 es2))
   1.259 +    
   1.260  fun defnode_edges_foldl f a defnode =
   1.261      let
   1.262 -	val (Defnode (ty, def_edges)) = defnode
   1.263 -	fun g (b, (_, (n, labelled_edges))) =
   1.264 -	    foldl (fn ((s, edges), b') => 
   1.265 -		      (foldl (fn (e, b'') => f ty n s e b'') b' edges))
   1.266 -		  b
   1.267 -		  labelled_edges		  		     
   1.268 +      val (Defnode (ty, def_edges)) = defnode
   1.269 +      fun g (b, (_, (n, labelled_edges))) =
   1.270 +	  foldl (fn ((s, edges), b') => 
   1.271 +		    (foldl (fn (e, b'') => f ty n s e b'') b' edges))
   1.272 +		b
   1.273 +		labelled_edges		  		     
   1.274      in
   1.275 -	Symtab.foldl g (a, def_edges)
   1.276 +      Symtab.foldl g (a, def_edges)
   1.277      end	
   1.278 -
   1.279 +    
   1.280  fun define (actions, graph) (name, ty) axname body =
   1.281      let
   1.282 -	val ty = checkT ty
   1.283 -	val body = map (fn (n,t) => (n, checkT t)) body		 
   1.284 -	val mainref = name
   1.285 -	val mainnode  = (case Symtab.lookup (graph, mainref) of 
   1.286 -			     NONE => def_err ("constant "^(quote mainref)^" is not declared")
   1.287 -			   | SOME n => n)
   1.288 -	val (Node (n, gty, defs, backs, finals)) = mainnode
   1.289 -	val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
   1.290 -	fun check_def (s, Defnode (ty', _)) = 
   1.291 -	    (if can_be_unified_r ty ty' then 
   1.292 -		 raise (CLASH (mainref, axname, s))
   1.293 -	     else if s = axname then
   1.294 -	         def_err "name of axiom is already used for another definition of this constant"
   1.295 -	     else false)	
   1.296 -	val _ = Symtab.exists check_def defs
   1.297 -(*	fun check_final finalty = 
   1.298 -	    (if can_be_unified_r finalty ty then
   1.299 -		 raise (FINAL (mainref, finalty))
   1.300 -	     else
   1.301 -		 true)
   1.302 -	val _ = forall check_final finals*)
   1.303 -	
   1.304 -	(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
   1.305 +      val ty = checkT ty
   1.306 +      val body = map (fn (n,t) => (n, checkT t)) body		 
   1.307 +      val mainref = name
   1.308 +      val mainnode  = (case Symtab.lookup (graph, mainref) of 
   1.309 +			 NONE => def_err ("constant "^mainref^" is not declared")
   1.310 +		       | SOME n => n)
   1.311 +      val (Node (n, gty, defs, backs, finals)) = mainnode
   1.312 +      val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
   1.313 +      fun check_def (s, Defnode (ty', _)) = 
   1.314 +	  (if can_be_unified_r ty ty' then 
   1.315 +	     raise (CLASH (mainref, axname, s))
   1.316 +	   else if s = axname then
   1.317 +	     def_err "name of axiom is already used for another definition of this constant"
   1.318 +	   else false)	
   1.319 +      val _ = Symtab.exists check_def defs
   1.320 +      fun check_final finalty = 
   1.321 +	  (if can_be_unified_r finalty ty then
   1.322 +	     raise (FINAL (mainref, finalty))
   1.323 +	   else
   1.324 +	     true)
   1.325 +      val _ = forall check_final finals
   1.326 +	             
   1.327 +      (* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
   1.328  
   1.329 -	(* body contains the constants that this constant definition depends on. For each element of body,
   1.330 -           the function make_edges_to calculates a group of edges that connect this constant with 
   1.331 -           the constant that is denoted by the element of the body *)
   1.332 -	fun make_edges_to (bodyn, bodyty) =
   1.333 +      (* body contains the constants that this constant definition depends on. For each element of body,
   1.334 +         the function make_edges_to calculates a group of edges that connect this constant with 
   1.335 +         the constant that is denoted by the element of the body *)
   1.336 +      fun make_edges_to (bodyn, bodyty) =
   1.337 +	  let
   1.338 +	    val bnode = 
   1.339 +		(case Symtab.lookup (graph, bodyn) of 
   1.340 +		   NONE => def_err "body of constant definition references undeclared constant"
   1.341 +		 | SOME x => x)
   1.342 +	    val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode
   1.343 +	  in
   1.344 +	    case unify_r 0 bodyty general_btyp of
   1.345 +	      NONE => NONE
   1.346 +	    | SOME (maxidx, sigma1, sigma2) => 
   1.347 +	      SOME (
   1.348 +	      let
   1.349 +		(* For each definition of the constant in the body, 
   1.350 +		   check if the definition unifies with the type of the constant in the body. *)	                
   1.351 +                fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) =
   1.352 +		    if swallowed then
   1.353 +		      (swallowed, l)
   1.354 +		    else 
   1.355 +		      (case unify_r 0 bodyty def_ty of
   1.356 +			 NONE => (swallowed, l)
   1.357 +		       | SOME (maxidx, sigma1, sigma2) => 
   1.358 +			 (is_instance_r bodyty def_ty,
   1.359 +			  merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
   1.360 +                val swallowed = exists (is_instance_r bodyty) bfinals
   1.361 +          	val (swallowed, edges) = Symtab.foldl make_edges ((swallowed, []), bdefs)
   1.362 +	      in
   1.363 +		if swallowed then 
   1.364 +		  (bodyn, edges)
   1.365 +		else 
   1.366 +		  (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
   1.367 +	      end)
   1.368 +	  end 
   1.369 +          
   1.370 +      fun update_edges (b as (bodyn, bodyty), edges) =
   1.371 +	  (case make_edges_to b of
   1.372 +	     NONE => edges
   1.373 +	   | SOME m =>
   1.374 +	     (case Symtab.lookup (edges, bodyn) of
   1.375 +		NONE => Symtab.update ((bodyn, m), edges)
   1.376 +	      | SOME (_, es') => 
   1.377 +		let 
   1.378 +		  val (_, es) = m
   1.379 +		  val es = merge_labelled_edges es es'
   1.380 +		in
   1.381 +		  Symtab.update ((bodyn, (bodyn, es)), edges)
   1.382 +		end
   1.383 +	     )
   1.384 +	  )
   1.385 +          
   1.386 +      val edges = foldl update_edges Symtab.empty body
   1.387 +                  
   1.388 +      fun insert_edge edges (nodename, (defname_opt, edge)) = 
   1.389 +	  let
   1.390 +	    val newlink = [(defname_opt, [edge])]
   1.391 +	  in
   1.392 +	    case Symtab.lookup (edges, nodename) of
   1.393 +	      NONE => Symtab.update ((nodename, (nodename, newlink)), edges)		    
   1.394 +	    | SOME (_, links) => 
   1.395 +	      let
   1.396 +		val links' = merge_labelled_edges links newlink
   1.397 +	      in
   1.398 +		Symtab.update ((nodename, (nodename, links')), edges)
   1.399 +	      end
   1.400 +	  end				    
   1.401 +            
   1.402 +      (* We constructed all direct edges that this defnode has. 
   1.403 +         Now we have to construct the transitive hull by going a single step further. *)
   1.404 +          
   1.405 +      val thisDefnode = Defnode (ty, edges)
   1.406 +                        
   1.407 +      fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
   1.408 +	  case defname_opt of 
   1.409 +	    NONE => edges
   1.410 +	  | SOME defname => 		
   1.411  	    let
   1.412 -		val bnode = 
   1.413 -		    (case Symtab.lookup (graph, bodyn) of 
   1.414 -			 NONE => def_err "body of constant definition references undeclared constant"
   1.415 -		       | SOME x => x)
   1.416 -		val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode
   1.417 -	    in
   1.418 -		case unify_r 0 bodyty general_btyp of
   1.419 -		    NONE => NONE
   1.420 -		  | SOME (maxidx, sigma1, sigma2) => 
   1.421 -		    SOME (
   1.422 -		    let
   1.423 -			(* For each definition of the constant in the body, 
   1.424 -			   check if the definition unifies with the type of the constant in the body. *)	                
   1.425 -	              fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) =
   1.426 -			  if swallowed then
   1.427 -			      (swallowed, l)
   1.428 -			  else 
   1.429 -			      (case unify_r 0 bodyty def_ty of
   1.430 -				   NONE => (swallowed, l)
   1.431 -				 | SOME (maxidx, sigma1, sigma2) => 
   1.432 -				   (is_instance_r bodyty def_ty,
   1.433 -				    merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
   1.434 -          	      val (swallowed, edges) = Symtab.foldl make_edges ((false, []), bdefs)
   1.435 -		    in
   1.436 -			if swallowed (*orelse (exists (is_instance_r bodyty) bfinals)*) then 
   1.437 -			    (bodyn, edges)
   1.438 -			else 
   1.439 -			    (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
   1.440 -		    end)
   1.441 -	    end 
   1.442 -
   1.443 -	fun update_edges (b as (bodyn, bodyty), edges) =
   1.444 -	    (case make_edges_to b of
   1.445 -		 NONE => edges
   1.446 -	       | SOME m =>
   1.447 -		 (case Symtab.lookup (edges, bodyn) of
   1.448 -		      NONE => Symtab.update ((bodyn, m), edges)
   1.449 -		    | SOME (_, es') => 
   1.450 -		      let 
   1.451 -			  val (_, es) = m
   1.452 -			  val es = merge_labelled_edges es es'
   1.453 -		      in
   1.454 -			  Symtab.update ((bodyn, (bodyn, es)), edges)
   1.455 -		      end
   1.456 -		 )
   1.457 -	    )
   1.458 -
   1.459 -	val edges = foldl update_edges Symtab.empty body
   1.460 -
   1.461 -	fun insert_edge edges (nodename, (defname_opt, edge)) = 
   1.462 -	    let
   1.463 -		val newlink = [(defname_opt, [edge])]
   1.464 +	      val defnode = the (get_defnode' graph noderef defname)
   1.465 +	      fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges =
   1.466 +		  case unify_r (Int.max (max1, max2)) beta1 alpha2 of
   1.467 +		    NONE => edges
   1.468 +		  | SOME (max, sleft, sright) =>
   1.469 +		    insert_edge edges (noderef2, 
   1.470 +				       (defname_opt2, 							  
   1.471 +					(max, subst sleft alpha1, subst sright beta2, 
   1.472 +					 (subst_history sleft history1)@
   1.473 +					 ((subst sleft beta1, noderef, defname)::
   1.474 +					  (subst_history sright history2)))))
   1.475  	    in
   1.476 -		case Symtab.lookup (edges, nodename) of
   1.477 -		    NONE => Symtab.update ((nodename, (nodename, newlink)), edges)		    
   1.478 -		  | SOME (_, links) => 
   1.479 -		    let
   1.480 -			val links' = merge_labelled_edges links newlink
   1.481 -		    in
   1.482 -			Symtab.update ((nodename, (nodename, links')), edges)
   1.483 -		    end
   1.484 -	    end				    
   1.485 -
   1.486 -        (* We constructed all direct edges that this defnode has. 
   1.487 -           Now we have to construct the transitive hull by going a single step further. *)
   1.488 -
   1.489 -        val thisDefnode = Defnode (ty, edges)
   1.490 +	      defnode_edges_foldl make_trans_edge edges defnode
   1.491 +	    end
   1.492 +            
   1.493 +      val edges = defnode_edges_foldl make_trans_edges edges thisDefnode
   1.494 +                  
   1.495 +      val thisDefnode = Defnode (ty, edges)
   1.496  
   1.497 -	fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
   1.498 -	    case defname_opt of 
   1.499 -		NONE => edges
   1.500 -	      | SOME defname => 		
   1.501 -		let
   1.502 -		    val defnode = the (get_defnode' graph noderef defname)
   1.503 -		    fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges =
   1.504 -			case unify_r (Int.max (max1, max2)) beta1 alpha2 of
   1.505 -			    NONE => edges
   1.506 -			  | SOME (max, sleft, sright) =>
   1.507 -			    insert_edge edges (noderef2, 
   1.508 -					       (defname_opt2, 							  
   1.509 -						(max, subst sleft alpha1, subst sright beta2, 
   1.510 -						 (subst_history sleft history1)@
   1.511 -						 ((subst sleft beta1, noderef, defname)::
   1.512 -						  (subst_history sright history2)))))
   1.513 -		in
   1.514 -		    defnode_edges_foldl make_trans_edge edges defnode
   1.515 -		end
   1.516 -
   1.517 -	val edges = defnode_edges_foldl make_trans_edges edges thisDefnode
   1.518 -
   1.519 -	val thisDefnode = Defnode (ty, edges)
   1.520 -
   1.521 -	(* We also have to add the backreferences that this new defnode induces. *)
   1.522 +      (* We also have to add the backreferences that this new defnode induces. *)
   1.523  	    
   1.524 -	fun hasNONElink ((NONE, _)::_) = true
   1.525 -	  | hasNONElink _ = false
   1.526 -	
   1.527 -	fun install_backref graph noderef pointingnoderef pointingdefname = 
   1.528 -	    let
   1.529 -		val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
   1.530 -		val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
   1.531 -	    in
   1.532 -		case Symtab.lookup (backs, pname) of
   1.533 -		    NONE => 
   1.534 -		    let 
   1.535 -			val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
   1.536 -			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   1.537 -		    in
   1.538 -			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 			
   1.539 -		    end
   1.540 -		  | SOME (Backref (pointingnoderef, defnames)) =>
   1.541 -		    let
   1.542 -			val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
   1.543 -			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   1.544 -		    in
   1.545 -			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
   1.546 -		    end
   1.547 -		    handle Symtab.DUP _ => graph
   1.548 -	    end
   1.549 -
   1.550 -	fun install_backrefs (graph, (_, (noderef, labelled_edges))) =
   1.551 -	    if hasNONElink labelled_edges then
   1.552 -		install_backref graph noderef mainref axname
   1.553 -	    else 
   1.554 -		graph
   1.555 -
   1.556 -        val graph = Symtab.foldl install_backrefs (graph, edges)
   1.557 -
   1.558 -        val (Node (_, _, _, backs, _)) = getnode graph mainref
   1.559 -	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
   1.560 -          ((axname, thisDefnode), defs), backs, finals)), graph)
   1.561 -		    
   1.562 -	(* Now we have to check all backreferences to this node and inform them about the new defnode. 
   1.563 -	   In this section we also check for circularity. *)
   1.564 -        fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) =	    
   1.565 -	    let
   1.566 -		val node = getnode graph noderef
   1.567 -		fun update_defs ((defnames, newedges),(defname, _)) =
   1.568 +      fun hasNONElink ((NONE, _)::_) = true
   1.569 +	| hasNONElink _ = false
   1.570 +	                  
   1.571 +      fun install_backref graph noderef pointingnoderef pointingdefname = 
   1.572 +	  let
   1.573 +	    val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
   1.574 +	    val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
   1.575 +	  in
   1.576 +	    case Symtab.lookup (backs, pname) of
   1.577 +	      NONE => 
   1.578 +	      let 
   1.579 +		val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
   1.580 +		val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   1.581 +	      in
   1.582 +		Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 			
   1.583 +	      end
   1.584 +	    | SOME (Backref (pointingnoderef, defnames)) =>
   1.585 +	      let
   1.586 +		val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
   1.587 +		val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   1.588 +	      in
   1.589 +		Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
   1.590 +	      end
   1.591 +	      handle Symtab.DUP _ => graph
   1.592 +	  end
   1.593 +          
   1.594 +      fun install_backrefs (graph, (_, (noderef, labelled_edges))) =
   1.595 +	  if hasNONElink labelled_edges then
   1.596 +	    install_backref graph noderef mainref axname
   1.597 +	  else 
   1.598 +	    graph
   1.599 +            
   1.600 +      val graph = Symtab.foldl install_backrefs (graph, edges)
   1.601 +                  
   1.602 +      val (Node (_, _, _, backs, _)) = getnode graph mainref
   1.603 +      val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
   1.604 +        ((axname, thisDefnode), defs), backs, finals)), graph)
   1.605 +		                
   1.606 +      (* Now we have to check all backreferences to this node and inform them about the new defnode. 
   1.607 +	 In this section we also check for circularity. *)
   1.608 +      fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) =	    
   1.609 +	  let
   1.610 +	    val node = getnode graph noderef
   1.611 +	    fun update_defs ((defnames, newedges),(defname, _)) =
   1.612 +		let
   1.613 +		  val (Defnode (_, defnode_edges)) = the (get_defnode node defname)
   1.614 +		  val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n))
   1.615 +						
   1.616 +	          (* the type of thisDefnode is ty *)
   1.617 +		  fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
   1.618 +		      case unify_r max beta ty of
   1.619 +			NONE => (e::none_edges, this_edges)
   1.620 +		      | SOME (max', s_beta, s_ty) =>
   1.621 +			let
   1.622 +			  val alpha' = subst s_beta alpha
   1.623 +			  val ty' = subst s_ty ty				      
   1.624 +			  val _ = 
   1.625 +			      if noderef = mainref andalso defname = axname then
   1.626 +				(case unify alpha' ty' of
   1.627 +				   NONE => 
   1.628 +				   if (is_instance_r ty' alpha') then
   1.629 +				     raise (INFINITE_CHAIN (
   1.630 +					    (alpha', mainref, axname)::
   1.631 +					    (subst_history s_beta history)@
   1.632 +					    [(ty', mainref, axname)]))
   1.633 +				   else ()
   1.634 +				 | SOME s => raise (CIRCULAR (
   1.635 +						    (subst s alpha', mainref, axname)::
   1.636 +						    (subst_history s (subst_history s_beta history))@
   1.637 +						    [(subst s ty', mainref, axname)])))
   1.638 +			      else ()
   1.639 +			  val edge = (max', alpha', ty', subst_history s_beta history)
   1.640 +			in
   1.641 +			  if is_instance_r beta ty then 
   1.642 +			    (none_edges, edge::this_edges)
   1.643 +			  else
   1.644 +			    (e::none_edges, edge::this_edges)
   1.645 +			end					    			   			    
   1.646 +		in
   1.647 +		  case labelled_edges of 
   1.648 +		    ((NONE, edges)::_) => 
   1.649  		    let
   1.650 -			val (Defnode (_, defnode_edges)) = the (get_defnode node defname)
   1.651 -			val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n))
   1.652 -						      
   1.653 -			(* the type of thisDefnode is ty *)
   1.654 -			fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
   1.655 -			    case unify_r max beta ty of
   1.656 -				NONE => (e::none_edges, this_edges)
   1.657 -			      | SOME (max', s_beta, s_ty) =>
   1.658 -				let
   1.659 -				    val alpha' = subst s_beta alpha
   1.660 -				    val ty' = subst s_ty ty				      
   1.661 -				    val _ = 
   1.662 -					if noderef = mainref andalso defname = axname then
   1.663 -					    (case unify alpha' ty' of
   1.664 -						 NONE => 
   1.665 -						   if (is_instance_r ty' alpha') then
   1.666 -						       raise (INFINITE_CHAIN (
   1.667 -							      (alpha', mainref, axname)::
   1.668 -							      (subst_history s_beta history)@
   1.669 -							      [(ty', mainref, axname)]))
   1.670 -						   else ()
   1.671 -					       | SOME s => raise (CIRCULAR (
   1.672 -								  (subst s alpha', mainref, axname)::
   1.673 -								  (subst_history s (subst_history s_beta history))@
   1.674 -								  [(subst s ty', mainref, axname)])))
   1.675 -					else ()
   1.676 -				    val edge = (max', alpha', ty', subst_history s_beta history)
   1.677 -				in
   1.678 -				    if is_instance_r beta ty then 
   1.679 -					(none_edges, edge::this_edges)
   1.680 -				    else
   1.681 -					(e::none_edges, edge::this_edges)
   1.682 -				end					    			   			    
   1.683 +		      val (none_edges, this_edges) = foldl update ([], []) edges
   1.684 +		      val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
   1.685  		    in
   1.686 -			case labelled_edges of 
   1.687 -			    ((NONE, edges)::_) => 
   1.688 -			    let
   1.689 -				val (none_edges, this_edges) = foldl update ([], []) edges
   1.690 -				val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
   1.691 -			    in
   1.692 -				(defnames, (defname, none_edges, this_edges)::newedges)
   1.693 -			    end			    
   1.694 -			  | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
   1.695 -		    end
   1.696 +		      (defnames, (defname, none_edges, this_edges)::newedges)
   1.697 +		    end			    
   1.698 +		  | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
   1.699 +		end
   1.700  		    
   1.701 -		val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
   1.702 -	    in
   1.703 -		if Symtab.is_empty defnames then 
   1.704 -		    (backs, (noderef, newedges')::newedges)
   1.705 -		else
   1.706 -		    let
   1.707 -			val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs)
   1.708 -		    in
   1.709 -			(backs, newedges)
   1.710 -		    end
   1.711 -	    end
   1.712 -	    
   1.713 -
   1.714 -	val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs)
   1.715 -						 
   1.716 -	(* If a Circular exception is thrown then we never reach this point. *)
   1.717 -        (* Ok, the definition is consistent, let's update this node. *)
   1.718 -	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
   1.719 -	  ((axname, thisDefnode), defs), backs, finals)), graph)
   1.720 +	    val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
   1.721 +	  in
   1.722 +	    if Symtab.is_empty defnames then 
   1.723 +	      (backs, (noderef, newedges')::newedges)
   1.724 +	    else
   1.725 +	      let
   1.726 +		val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs)
   1.727 +	      in
   1.728 +		(backs, newedges)
   1.729 +	      end
   1.730 +	  end
   1.731 +	  
   1.732  
   1.733 -        (* Furthermore, update all the other nodes that backreference this node. *)
   1.734 -        fun final_update_backrefs graph noderef defname none_edges this_edges =
   1.735 -	    let
   1.736 -		val node = getnode graph noderef
   1.737 -		val (Node (nodename, nodety, defs, backs, finals)) = node
   1.738 -		val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
   1.739 -		val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
   1.740 -
   1.741 -		fun update edges none_edges this_edges =
   1.742 -		    let 
   1.743 -			val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)]
   1.744 -		    in
   1.745 -			if none_edges = [] then
   1.746 -			    u
   1.747 -			else
   1.748 -			    (NONE, pack_edges none_edges)::u
   1.749 -		    end
   1.750 -		    
   1.751 -		val defnode_links' = 
   1.752 -		    case defnode_links of 
   1.753 -			((NONE, _) :: edges) => update edges none_edges this_edges
   1.754 -		      | edges => update edges none_edges this_edges
   1.755 -		val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
   1.756 -		val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
   1.757 -	    in
   1.758 -		Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
   1.759 -	    end
   1.760 +      val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs)
   1.761 +						 
   1.762 +      (* If a Circular exception is thrown then we never reach this point. *)
   1.763 +      (* Ok, the definition is consistent, let's update this node. *)
   1.764 +      val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
   1.765 +        ((axname, thisDefnode), defs), backs, finals)), graph)
   1.766  
   1.767 -	val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
   1.768 -           final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges		    
   1.769 -
   1.770 +      (* Furthermore, update all the other nodes that backreference this node. *)
   1.771 +      fun final_update_backrefs graph noderef defname none_edges this_edges =
   1.772 +	  let
   1.773 +	    val node = getnode graph noderef
   1.774 +	    val (Node (nodename, nodety, defs, backs, finals)) = node
   1.775 +	    val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
   1.776 +	    val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
   1.777 +                                     
   1.778 +	    fun update edges none_edges this_edges =
   1.779 +		let 
   1.780 +		  val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)]
   1.781 +		in
   1.782 +		  if none_edges = [] then
   1.783 +		    u
   1.784 +		  else
   1.785 +		    (NONE, pack_edges none_edges)::u
   1.786 +		end
   1.787 +		
   1.788 +	    val defnode_links' = 
   1.789 +		case defnode_links of 
   1.790 +		  ((NONE, _) :: edges) => update edges none_edges this_edges
   1.791 +		| edges => update edges none_edges this_edges
   1.792 +	    val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
   1.793 +	    val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
   1.794 +	  in
   1.795 +	    Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
   1.796 +	  end
   1.797 +          
   1.798 +      val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
   1.799 +        final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges		    
   1.800 +                  
   1.801      in	    
   1.802 -	((Define (name, ty, axname, body))::actions, graph)	   
   1.803 +      ((Define (name, ty, axname, body))::actions, graph)	   
   1.804      end 
   1.805 -
   1.806 -    fun finalize' ((c, ty), graph) = 
   1.807 -      case Symtab.lookup (graph, c) of 
   1.808 -	  NONE => def_err ("cannot finalize constant "^(quote c)^"; it is not declared")
   1.809 -	| SOME (Node (noderef, nodety, defs, backs, finals)) =>
   1.810 -	  let 
   1.811 -	      val ty = checkT ty
   1.812 -	      val _ = if (not (is_instance_r ty nodety)) then
   1.813 -			  def_err ("only type instances of the declared constant "^(quote c)^" can be finalized")
   1.814 -		      else ()
   1.815 -	      val _ = Symtab.exists (fn (def_name, Defnode (def_ty, _)) =>  
   1.816 -					if can_be_unified_r ty def_ty then 
   1.817 -					    def_err ("cannot finalize constant "^(quote c)^"; clash with definition "^(quote def_name))
   1.818 -					else 
   1.819 -					    false)
   1.820 -				    defs
   1.821 -	  in				    
   1.822 -	      if exists (is_instance_r ty) finals then
   1.823 -		  graph
   1.824 -	      else 
   1.825 -	      let
   1.826 -	          val finals = ty :: finals
   1.827 -		  val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
   1.828 -	      in
   1.829 -		  graph
   1.830 -	      end
   1.831 -(*		  fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
   1.832 -		  let
   1.833 -		      fun update_backdef ((graph, defnames), (backdefname, _)) = 
   1.834 +    
   1.835 +fun finalize (history, graph) (c, ty) = 
   1.836 +    case Symtab.lookup (graph, c) of 
   1.837 +      NONE => def_err ("cannot finalize constant "^c^"; it is not declared")
   1.838 +    | SOME (Node (noderef, nodety, defs, backs, finals)) =>
   1.839 +      let 
   1.840 +	val ty = checkT ty
   1.841 +	val _ = if (not (is_instance_r ty nodety)) then
   1.842 +		  def_err ("only type instances of the declared constant "^c^" can be finalized")
   1.843 +		else ()
   1.844 +	val _ = Symtab.exists (fn (def_name, Defnode (def_ty, _)) =>  
   1.845 +				  if can_be_unified_r ty def_ty then 
   1.846 +				    def_err ("cannot finalize constant "^c^"; clash with definition "^def_name)
   1.847 +				  else 
   1.848 +				    false)
   1.849 +			      defs 
   1.850 +        
   1.851 +        fun update_finals [] = SOME [ty]
   1.852 +          | update_finals (final_ty::finals) = 
   1.853 +            (if is_instance_r ty final_ty then NONE
   1.854 +             else
   1.855 +               case update_finals finals of
   1.856 +                 NONE => NONE
   1.857 +               | (r as SOME finals) =>
   1.858 +                 if (is_instance_r final_ty ty) then
   1.859 +                   r
   1.860 +                 else
   1.861 +                   SOME (final_ty :: finals))                              
   1.862 +      in    
   1.863 +        case update_finals finals of
   1.864 +          NONE => (history, graph)
   1.865 +        | SOME finals => 
   1.866 +	  let
   1.867 +	    val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
   1.868 +	                
   1.869 +	    fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
   1.870 +		let
   1.871 +		  fun update_backdef ((graph, defnames), (backdefname, _)) = 
   1.872  	              let 
   1.873 -			  val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
   1.874 -			  val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)						      
   1.875 -			  val (defnames', all_edges') = 
   1.876 -			      case Symtab.lookup (all_edges, noderef) of
   1.877 -				  NONE => sys_error "finalize: corrupt backref"
   1.878 -				| SOME (_, (NONE, edges)::rest) =>
   1.879 -				  let
   1.880 -				      val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
   1.881 -				  in
   1.882 -				      if edges' = [] then 
   1.883 -					  (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
   1.884 -				      else
   1.885 -					  (Symtab.update ((backdefname, ()), defnames), 
   1.886 -					   Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
   1.887 -				  end
   1.888 -			  val defnode' = Defnode (def_ty, all_edges')
   1.889 -			  val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
   1.890 -					   backbacks, backfinals)
   1.891 +			val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
   1.892 +			val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)						      
   1.893 +			val (defnames', all_edges') = 
   1.894 +			    case Symtab.lookup (all_edges, noderef) of
   1.895 +			      NONE => sys_error "finalize: corrupt backref"
   1.896 +			    | SOME (_, (NONE, edges)::rest) =>
   1.897 +			      let
   1.898 +				val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
   1.899 +			      in
   1.900 +				if edges' = [] then 
   1.901 +				  (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
   1.902 +				else
   1.903 +				  (Symtab.update ((backdefname, ()), defnames), 
   1.904 +				   Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
   1.905 +			      end
   1.906 +			val defnode' = Defnode (def_ty, all_edges')
   1.907 +			val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
   1.908 +					      backbacks, backfinals)
   1.909  		      in
   1.910 -			  (Symtab.update ((backrefname, backnode'), graph), defnames')			  			  
   1.911 +			(Symtab.update ((backrefname, backnode'), graph), defnames')			  			  
   1.912  		      end
   1.913 -	  
   1.914 -		      val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   1.915 -		  in
   1.916 -		      (graph', if Symtab.is_empty defnames' then backs 
   1.917 -			       else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
   1.918 -		  end
   1.919 -		  val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   1.920 -		  val Node (_, _, defs, _, _) = getnode graph' noderef
   1.921 -	      in
   1.922 -		  Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph')
   1.923 -	      end*)
   1.924 +	              
   1.925 +		  val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   1.926 +		in
   1.927 +		  (graph', if Symtab.is_empty defnames' then backs 
   1.928 +			   else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
   1.929 +		end
   1.930 +	    val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   1.931 +	    val Node (_, _, defs, _, _) = getnode graph' noderef
   1.932 +	  in
   1.933 +	    ((Finalize (c, ty)) :: history, Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph'))
   1.934  	  end
   1.935 -	   
   1.936 -    fun finalize (history, graph) c_ty = (history, graph)
   1.937 -	(*((Finalize c_ty)::history, finalize' (c_ty, graph))*)
   1.938 -    
   1.939 -    fun merge' (Declare cty, g) = (declare g cty handle _ => g)
   1.940 -      | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
   1.941 -	(case Symtab.lookup (graph, name) of
   1.942 -	     NONE => define g (name, ty) axname body
   1.943 -	   | SOME (Node (_, _, defs, _, _)) => 
   1.944 -	     (case Symtab.lookup (defs, axname) of
   1.945 -		  NONE => define g (name, ty) axname body
   1.946 -		| SOME _ => g))
   1.947 -      | merge' (Finalize finals, g) = (finalize g finals handle _ => g)
   1.948 -	
   1.949 -    fun myrev [] ys = ys
   1.950 -      | myrev (x::xs) ys = myrev xs (x::ys)
   1.951 -
   1.952 -    fun merge (actions, _) g = foldr merge' g actions
   1.953 -
   1.954 -    fun finals (history, graph) = 
   1.955 -	Symtab.foldl 
   1.956 -	    (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
   1.957 -	    (Symtab.empty, graph)
   1.958 +      end
   1.959 +      
   1.960 +fun merge' (Declare cty, g) = (declare g cty handle _ => g)
   1.961 +  | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
   1.962 +    (case Symtab.lookup (graph, name) of
   1.963 +       NONE => define g (name, ty) axname body
   1.964 +     | SOME (Node (_, _, defs, _, _)) => 
   1.965 +       (case Symtab.lookup (defs, axname) of
   1.966 +	  NONE => define g (name, ty) axname body
   1.967 +	| SOME _ => g))
   1.968 +  | merge' (Finalize finals, g) = finalize g finals 
   1.969 +                       
   1.970 +fun merge (actions, _) g = foldr merge' g actions
   1.971 +                           
   1.972 +fun finals (history, graph) = 
   1.973 +    Symtab.foldl 
   1.974 +      (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
   1.975 +      (Symtab.empty, graph)
   1.976  
   1.977  end;
   1.978