# HG changeset patch # User wenzelm # Date 1120672829 -7200 # Node ID 040728f6a1030a57e4bba68907bc63a2b448ab55 # Parent e2427ea379a9ec50e71f554c0e15f299bbfc57ee tuned forall_elim_var(s): avoid expensive Term.add_vars; diff -r e2427ea379a9 -r 040728f6a103 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed Jul 06 20:00:27 2005 +0200 +++ b/src/Pure/pure_thy.ML Wed Jul 06 20:00:29 2005 +0200 @@ -389,22 +389,24 @@ end; -(* forall_elim_vars (belongs to drule.ML) *) +(* forall_elim_var(s) -- belongs to drule.ML *) -(*Replace outermost quantified variable by Var of given index.*) -fun forall_elim_var i th = - let val {prop, thy, ...} = Thm.rep_thm th - in case prop of - Const ("all", _) $ Abs (a, T, _) => - let val used = map (fst o fst) - (List.filter (equal i o snd o fst) (Term.add_vars ([], prop))) - in Thm.forall_elim (Thm.cterm_of thy (Var ((variant used a, i), T))) th end - | _ => raise THM ("forall_elim_var", i, [th]) - end; +fun forall_elim_vars_aux strip_vars i th = + let + val {thy, tpairs, prop, ...} = Thm.rep_thm th; + fun add_used t used = (used, t) |> Term.foldl_aterms + (fn (xs, Var ((x, j), _)) => if i = j then x ins_string xs else xs | (xs, _) => xs); + val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []); + val vars = strip_vars prop; + val cvars = (Term.variantlist (map #1 vars, used), vars) + |> ListPair.map (fn (x, (_, T)) => Thm.cterm_of thy (Var ((x, i), T))); + in fold Thm.forall_elim cvars th end; -(*Repeat forall_elim_var until all outer quantifiers are removed*) -fun forall_elim_vars i th = - forall_elim_vars i (forall_elim_var i th) handle THM _ => th; +val forall_elim_vars = forall_elim_vars_aux Term.strip_all_vars; + +fun forall_elim_var i th = forall_elim_vars_aux + (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)] + | _ => raise THM ("forall_elim_vars", i, [th])) i th; (* store axioms as theorems *)