Changed subst_bounds to subst_bound, to run faster
authorpaulson
Mon Nov 18 16:30:06 1996 +0100 (1996-11-18)
changeset 2193b7e59795c75b
parent 2192 3bf092b5310b
child 2194 63a68a3a8a76
Changed subst_bounds to subst_bound, to run faster
src/Pure/thm.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/thm.ML	Mon Nov 18 16:28:40 1996 +0100
     1.2 +++ b/src/Pure/thm.ML	Mon Nov 18 16:30:06 1996 +0100
     1.3 @@ -781,7 +781,7 @@
     1.4  		 maxidx = maxidx,
     1.5  		 shyps = [],
     1.6  		 hyps = [],
     1.7 -		 prop = Logic.mk_equals(t, subst_bounds([u],bodt))})
     1.8 +		 prop = Logic.mk_equals(t, subst_bound (u,bodt))})
     1.9          | _ =>  raise THM("beta_conversion: not a redex", 0, [])
    1.10    end;
    1.11  
    1.12 @@ -1643,7 +1643,7 @@
    1.13        end
    1.14    in case etat of
    1.15         Abs(_,_,body) $ u => Some(shypst, hypst, maxt, 
    1.16 -				 subst_bounds([u], body),
    1.17 +				 subst_bound (u, body),
    1.18  				 ders)
    1.19       | _                 => rews (sort_rrules (Net.match_term net etat))
    1.20    end;
    1.21 @@ -1710,7 +1710,7 @@
    1.22  		 val mss' = Mss{net=net, congs=congs, bounds=b::bounds,
    1.23  				prems=prems,mk_rews=mk_rews}
    1.24  	     in case botc true mss' 
    1.25 -		       (shyps,hyps,maxidx,subst_bounds([v],t),ders) of
    1.26 +		       (shyps,hyps,maxidx,subst_bound (v,t),ders) of
    1.27  		  Some(shyps',hyps',maxidx',t',ders') =>
    1.28  		    Some(shyps', hyps', maxidx',
    1.29  			 Abs(a, T, abstract_over(v,t')),
    1.30 @@ -1720,7 +1720,7 @@
    1.31  	 | t$u => (case t of
    1.32  	     Const("==>",_)$s  => Some(impc(shyps,hyps,maxidx,s,u,mss,ders))
    1.33  	   | Abs(_,_,body) =>
    1.34 -	       let val trec = (shyps,hyps,maxidx,subst_bounds([u],body),ders)
    1.35 +	       let val trec = (shyps,hyps,maxidx,subst_bound (u,body),ders)
    1.36  	       in case subc mss trec of
    1.37  		    None => Some(trec)
    1.38  		  | trec => trec
     2.1 --- a/src/Pure/unify.ML	Mon Nov 18 16:28:40 1996 +0100
     2.2 +++ b/src/Pure/unify.ML	Mon Nov 18 16:30:06 1996 +0100
     2.3 @@ -85,11 +85,11 @@
     2.4  		| None   => raise SAME)
     2.5  	  | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
     2.6  	  | hnorm (Abs(_,_,body) $ t) =
     2.7 -	      head_norm (env, subst_bounds([t], body))
     2.8 +	      head_norm (env, subst_bound (t, body))
     2.9  	  | hnorm (f $ t) =
    2.10  	      (case hnorm f of
    2.11  		 Abs(_,_,body) =>
    2.12 -		   head_norm (env, subst_bounds([t], body))
    2.13 +		   head_norm (env, subst_bound (t, body))
    2.14  	       | nf => nf $ t)
    2.15  	  | hnorm _ =  raise SAME
    2.16      in  hnorm t  handle SAME=> t  end