1.1 --- a/src/Pure/pure_thy.ML	Thu Oct 21 18:41:51 1999 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Oct 21 18:42:38 1999 +0200
     1.3 @@ -28,6 +28,8 @@
     1.4    val thms_containing: theory -> string list -> (string * thm) list
     1.5    val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
     1.6    val smart_store_thms: (bstring * thm list) -> thm list
     1.7 +  val forall_elim_var: int -> thm -> thm
     1.8 +  val forall_elim_vars: int -> thm -> thm
     1.9    val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory
    1.10    val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory
    1.11    val have_thmss: bstring -> theory attribute list ->
    1.12 @@ -266,10 +268,29 @@
    1.13        in enter_thmx (Sign.deref sg_ref) name_multi (name, thms) end;
    1.14  
    1.15  
    1.16 +(* forall_elim_vars (belongs to drule.ML) *)
    1.17 +
    1.18 +(*Replace outermost quantified variable by Var of given index.
    1.19 +    Could clash with Vars already present.*)
    1.20 +fun forall_elim_var i th =
    1.21 +    let val {prop,sign,...} = rep_thm th
    1.22 +    in case prop of
    1.23 +          Const("all",_) $ Abs(a,T,_) =>
    1.24 +              forall_elim (cterm_of sign (Var((a,i), T)))  th
    1.25 +        | _ => raise THM("forall_elim_var", i, [th])
    1.26 +    end;
    1.27 +
    1.28 +(*Repeat forall_elim_var until all outer quantifiers are removed*)
    1.29 +fun forall_elim_vars i th =
    1.30 +    forall_elim_vars i (forall_elim_var i th)
    1.31 +        handle THM _ => th;
    1.32 +
    1.33 +
    1.34  (* store axioms as theorems *)
    1.35  
    1.36  local
    1.37 -  fun get_axs thy named_axs = map (Thm.get_axiom thy o fst) named_axs;
    1.38 +  fun get_axs thy named_axs =
    1.39 +    map (forall_elim_vars 0 o Thm.get_axiom thy o fst) named_axs;
    1.40  
    1.41    fun add_single add ((name, ax), atts) thy =
    1.42      let