src/Pure/drule.ML
changeset 26653 60e0cf6bef89
parent 26627 dac6d56b7c8d
child 26939 1035c89b4c02
     1.1 --- a/src/Pure/drule.ML	Tue Apr 15 16:12:01 2008 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Apr 15 16:12:05 2008 +0200
     1.3 @@ -25,8 +25,6 @@
     1.4    val forall_intr_frees: thm -> thm
     1.5    val forall_intr_vars: thm -> thm
     1.6    val forall_elim_list: cterm list -> thm -> thm
     1.7 -  val forall_elim_var: int -> thm -> thm
     1.8 -  val forall_elim_vars: int -> thm -> thm
     1.9    val gen_all: thm -> thm
    1.10    val lift_all: cterm -> thm -> thm
    1.11    val freeze_thaw: thm -> thm * (thm -> thm)
    1.12 @@ -290,9 +288,6 @@
    1.13    fold forall_intr
    1.14      (map (Thm.cterm_of (Thm.theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th [])) th;
    1.15  
    1.16 -val forall_elim_var = PureThy.forall_elim_var;
    1.17 -val forall_elim_vars = PureThy.forall_elim_vars;
    1.18 -
    1.19  fun outer_params t =
    1.20    let val vs = Term.strip_all_vars t
    1.21    in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
    1.22 @@ -373,7 +368,7 @@
    1.23    #> forall_intr_frees
    1.24    #> `Thm.maxidx_of
    1.25    #-> (fn maxidx =>
    1.26 -    forall_elim_vars (maxidx + 1)
    1.27 +    Thm.forall_elim_vars (maxidx + 1)
    1.28      #> Thm.strip_shyps
    1.29      #> zero_var_indexes
    1.30      #> Thm.varifyT);