# HG changeset patch
# User wenzelm
# Date 1152035390 -7200
# Node ID 9592df0c3176b1b96b56215ffb988a217aea4b2e
# Parent  c8018518e112cd0f0c192a2593b2310d9fddd946
added generalize;
removed obsolete assume_ax, tvars_intr_list;

diff -r c8018518e112 -r 9592df0c3176 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jul 04 19:49:49 2006 +0200
+++ b/src/Pure/drule.ML	Tue Jul 04 19:49:50 2006 +0200
@@ -43,7 +43,6 @@
   val standard': thm -> thm
   val rotate_prems: int -> thm -> thm
   val rearrange_prems: int list -> thm -> thm
-  val assume_ax: theory -> string -> thm
   val RSN: thm * (int * thm) -> thm
   val RS: thm * thm -> thm
   val RLN: thm list * (int * thm list) -> thm list
@@ -87,6 +86,7 @@
 signature DRULE =
 sig
   include BASIC_DRULE
+  val generalize: string list * string list -> thm -> thm
   val dest_binop: cterm -> cterm * cterm
   val list_comb: cterm * cterm list -> cterm
   val strip_comb: cterm -> cterm * cterm list
@@ -137,7 +137,6 @@
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
   val rename_bvars: (string * string) list -> thm -> thm
   val rename_bvars': string option list -> thm -> thm
-  val tvars_intr_list: string list -> thm -> (string * (indexname * sort)) list * thm
   val incr_indexes: thm -> thm -> thm
   val incr_indexes2: thm -> thm -> thm -> thm
   val remdups_rl: thm
@@ -401,6 +400,8 @@
     |> fold_rev (Thm.forall_intr o cert) ps
   end;
 
+(*direct generalization*)
+fun generalize names th = Thm.generalize names (Thm.maxidx_of th + 1) th;
 
 (*specialization over a list of cterms*)
 val forall_elim_list = fold forall_elim;
@@ -489,7 +490,7 @@
  end;
 
 (*Basic version of the function above. No option to rename Vars apart in thaw.
-  The Frees created from Vars have nice names. FIXME: does not check for 
+  The Frees created from Vars have nice names. FIXME: does not check for
   clashes with variables in the assumptions, so delete and use freeze_thaw_robust instead?*)
 fun freeze_thaw th =
  let val fth = Thm.freezeT th
@@ -526,15 +527,6 @@
      (permute_prems (new+1) (new-p) (permute_prems new (p-new) thm))
   in rearr 0 end;
 
-(*Assume a new formula, read following the same conventions as axioms.
-  Generalizes over Free variables,
-  creates the assumption, and then strips quantifiers.
-  Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
-             [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
-fun assume_ax thy sP =
-  let val prop = Logic.close_form (term_of (read_cterm thy (sP, propT)))
-  in forall_elim_vars 0 (Thm.assume (cterm_of thy prop)) end;
-
 (*Resolution: exactly one resolvent must be produced.*)
 fun tha RSN (i,thb) =
   case Seq.chop 2 (biresolution false [(false,tha)] i thb) of
@@ -1081,13 +1073,6 @@
   end;
 
 
-(* tvars_intr_list *)
-
-fun tvars_intr_list tfrees thm =
-  apfst (map (fn ((s, S), ixn) => (s, (ixn, S)))) (Thm.varifyT'
-    (gen_rems (op = o apfst fst) (tfrees_of thm, tfrees)) thm);
-
-
 (* var indexes *)
 
 fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);