generalized fixes get index 0;
authorwenzelm
Fri Jul 02 15:05:16 1999 +0200 (1999-07-02)
changeset 688712b5fb35a688
parent 6886 7d0f7ad5a35f
child 6888 d0c68ebdabc5
generalized fixes get index 0;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Jul 02 15:04:45 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Jul 02 15:05:16 1999 +0200
     1.3 @@ -329,12 +329,12 @@
     1.4  
     1.5      fun find_free t x = foldl_aterms (get_free x) (None, t);
     1.6  
     1.7 -    val {sign, maxidx, prop, ...} = Thm.rep_thm thm;
     1.8 +    val {sign, prop, ...} = Thm.rep_thm thm;
     1.9      val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) names);
    1.10    in
    1.11      thm
    1.12      |> Drule.forall_intr_list frees
    1.13 -    |> Drule.forall_elim_vars (maxidx + 1)
    1.14 +    |> Drule.forall_elim_vars 0
    1.15    end;
    1.16  
    1.17  fun varify_tfrees thm =