# HG changeset patch
# User wenzelm
# Date 1122556806 -7200
# Node ID ea65d75e0ce1e7d6a278f46c7e4264a89e028cb2
# Parent  3aef68881781350a634b2f59e65e0f070cb2caf1
tuned gen_all, forall_elim_list, implies_intr_list, standard;
impose_hyps: use Thm.weaken;
zero_var_indexes: use Term.zero_var_indexes_inst;
Sign.typ_unify;

diff -r 3aef68881781 -r ea65d75e0ce1 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jul 28 15:20:05 2005 +0200
+++ b/src/Pure/drule.ML	Thu Jul 28 15:20:06 2005 +0200
@@ -389,23 +389,21 @@
 fun gen_all thm =
   let
     val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
-    fun elim (th, (x, T)) = Thm.forall_elim (Thm.cterm_of thy (Var ((x, maxidx + 1), T))) th;
+    fun elim (x, T) = Thm.forall_elim (Thm.cterm_of thy (Var ((x, maxidx + 1), T)));
     val vs = Term.strip_all_vars prop;
-  in Library.foldl elim (thm, Term.variantlist (map #1 vs, []) ~~ map #2 vs) end;
+  in fold elim (Term.variantlist (map #1 vs, []) ~~ map #2 vs) thm end;
 
-(*Specialization over a list of cterms*)
-fun forall_elim_list cts th = foldr (uncurry forall_elim) th (rev cts);
+(*specialization over a list of cterms*)
+val forall_elim_list = fold forall_elim;
 
-(* maps A1,...,An |- B   to   [| A1;...;An |] ==> B  *)
-fun implies_intr_list cAs th = foldr (uncurry implies_intr) th cAs;
+(*maps A1,...,An |- B  to  [| A1;...;An |] ==> B*)
+val implies_intr_list = fold_rev implies_intr;
 
-(* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
+(*maps [| A1;...;An |] ==> B and [A1,...,An]  to  B*)
 fun implies_elim_list impth ths = Library.foldl (uncurry implies_elim) (impth,ths);
 
-(* maps |- B to A1,...,An |- B *)
-fun impose_hyps chyps th =
-  let val chyps' = gen_rems (op aconv o apfst Thm.term_of) (chyps, #hyps (Thm.rep_thm th))
-  in implies_elim_list (implies_intr_list chyps' th) (map Thm.assume chyps') end;
+(*maps |- B to A1,...,An |- B*)
+val impose_hyps = fold Thm.weaken;
 
 (* maps A1,...,An and A1,...,An |- B to |- B *)
 fun satisfy_hyps ths th =
@@ -413,26 +411,13 @@
 
 (*Reset Var indexes to zero, renaming to preserve distinctness*)
 fun zero_var_indexes th =
-    let val {prop,thy,tpairs,...} = rep_thm th;
-        val (tpair_l, tpair_r) = Library.split_list tpairs;
-        val vars = foldr add_term_vars 
-                         (foldr add_term_vars (term_vars prop) tpair_l) tpair_r;
-        val bs = Library.foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars)
-        val inrs = 
-            foldr add_term_tvars 
-                  (foldr add_term_tvars (term_tvars prop) tpair_l) tpair_r;
-        val nms' = rev(Library.foldl add_new_id ([], map (#1 o #1) inrs));
-        val tye = ListPair.map (fn ((v, rs), a) => (TVar (v, rs), TVar ((a, 0), rs)))
-                     (inrs, nms')
-        val ctye = map (pairself (ctyp_of thy)) tye;
-        fun varpairs([],[]) = []
-          | varpairs((var as Var(v,T)) :: vars, b::bs) =
-                let val T' = typ_subst_atomic tye T
-                in (cterm_of thy (Var(v,T')),
-                    cterm_of thy (Var((b,0),T'))) :: varpairs(vars,bs)
-                end
-          | varpairs _ = raise TERM("varpairs", []);
-    in Thm.instantiate (ctye, varpairs(vars,rev bs)) th end;
+  let
+    val thy = Thm.theory_of_thm th;
+    val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
+    val (instT, inst) = Term.zero_var_indexes_inst (Thm.full_prop_of th);
+    val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
+    val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
+  in Thm.adjust_maxidx_thm (Thm.instantiate (cinstT, cinst) th) end;
 
 
 (** Standard form of object-rule: no hypotheses, flexflex constraints,
@@ -454,20 +439,27 @@
   if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm)
   else thm;
 
-fun standard' th =
-  let val {maxidx,...} = rep_thm th in
-    th
-    |> implies_intr_hyps
-    |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
-    |> strip_shyps_warning
-    |> zero_var_indexes |> Thm.varifyT |> Thm.compress
-  end;
+val standard' =
+  implies_intr_hyps
+  #> forall_intr_frees
+  #> `(#maxidx o Thm.rep_thm)
+  #-> (fn maxidx =>
+    forall_elim_vars (maxidx + 1)
+    #> strip_shyps_warning
+    #> zero_var_indexes
+    #> Thm.varifyT
+    #> Thm.compress);
 
-val standard = close_derivation o standard' o flexflex_unique;
+val standard =
+  flexflex_unique
+  #> standard'
+  #> close_derivation;
 
-fun local_standard th =
-  th |> strip_shyps |> zero_var_indexes
-  |> Thm.compress |> close_derivation;
+val local_standard =
+  strip_shyps
+  #> zero_var_indexes
+  #> Thm.compress
+  #> close_derivation;
 
 
 (*Convert all Vars in a theorem to Frees.  Also return a function for
@@ -892,7 +884,7 @@
         and {thy=thyu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
         val maxi = Int.max(maxidx, Int.max(maxt, maxu));
         val thy' = Theory.merge(thy, Theory.merge(thyt, thyu))
-        val (tye',maxi') = Type.unify (Sign.tsig_of thy') (tye, maxi) (T, U)
+        val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi)
           handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
     in  (thy', tye', maxi')  end;
 in