# HG changeset patch
# User paulson
# Date 848331006 -3600
# Node ID b7e59795c75bc9831c5f5e5431914acae924997d
# Parent  3bf092b5310b9c8331c90fabd9eb85f57ab4a87a
Changed subst_bounds to subst_bound, to run faster

diff -r 3bf092b5310b -r b7e59795c75b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Nov 18 16:28:40 1996 +0100
+++ b/src/Pure/thm.ML	Mon Nov 18 16:30:06 1996 +0100
@@ -781,7 +781,7 @@
 		 maxidx = maxidx,
 		 shyps = [],
 		 hyps = [],
-		 prop = Logic.mk_equals(t, subst_bounds([u],bodt))})
+		 prop = Logic.mk_equals(t, subst_bound (u,bodt))})
         | _ =>  raise THM("beta_conversion: not a redex", 0, [])
   end;
 
@@ -1643,7 +1643,7 @@
       end
   in case etat of
        Abs(_,_,body) $ u => Some(shypst, hypst, maxt, 
-				 subst_bounds([u], body),
+				 subst_bound (u, body),
 				 ders)
      | _                 => rews (sort_rrules (Net.match_term net etat))
   end;
@@ -1710,7 +1710,7 @@
 		 val mss' = Mss{net=net, congs=congs, bounds=b::bounds,
 				prems=prems,mk_rews=mk_rews}
 	     in case botc true mss' 
-		       (shyps,hyps,maxidx,subst_bounds([v],t),ders) of
+		       (shyps,hyps,maxidx,subst_bound (v,t),ders) of
 		  Some(shyps',hyps',maxidx',t',ders') =>
 		    Some(shyps', hyps', maxidx',
 			 Abs(a, T, abstract_over(v,t')),
@@ -1720,7 +1720,7 @@
 	 | t$u => (case t of
 	     Const("==>",_)$s  => Some(impc(shyps,hyps,maxidx,s,u,mss,ders))
 	   | Abs(_,_,body) =>
-	       let val trec = (shyps,hyps,maxidx,subst_bounds([u],body),ders)
+	       let val trec = (shyps,hyps,maxidx,subst_bound (u,body),ders)
 	       in case subc mss trec of
 		    None => Some(trec)
 		  | trec => trec
diff -r 3bf092b5310b -r b7e59795c75b src/Pure/unify.ML
--- a/src/Pure/unify.ML	Mon Nov 18 16:28:40 1996 +0100
+++ b/src/Pure/unify.ML	Mon Nov 18 16:30:06 1996 +0100
@@ -85,11 +85,11 @@
 		| None   => raise SAME)
 	  | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
 	  | hnorm (Abs(_,_,body) $ t) =
-	      head_norm (env, subst_bounds([t], body))
+	      head_norm (env, subst_bound (t, body))
 	  | hnorm (f $ t) =
 	      (case hnorm f of
 		 Abs(_,_,body) =>
-		   head_norm (env, subst_bounds([t], body))
+		   head_norm (env, subst_bound (t, body))
 	       | nf => nf $ t)
 	  | hnorm _ =  raise SAME
     in  hnorm t  handle SAME=> t  end