1.1 --- a/src/Provers/eqsubst.ML	Wed Feb 15 21:34:55 2006 +0100
     1.2 +++ b/src/Provers/eqsubst.ML	Wed Feb 15 21:34:57 2006 +0100
     1.3 @@ -146,26 +146,11 @@
     1.4      in stepthms |> Seq.maps rewrite_with_thm end;
     1.5  
     1.6  
     1.7 -(* Tactic.distinct_subgoals_tac -- fails to free type variables *)
     1.8 +(* distinct subgoals *)
     1.9 +fun distinct_subgoals th =
    1.10 +  the_default th (SINGLE distinct_subgoals_tac th);
    1.11  
    1.12 -(* custom version of distinct subgoals that works with term and
    1.13 -   type variables. Asssumes th is in beta-eta normal form.
    1.14 -   Also, does nothing if flexflex contraints are present. *)
    1.15 -fun distinct_subgoals th =
    1.16 -    if List.null (Thm.tpairs_of th) then
    1.17 -      let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th
    1.18 -        val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm
    1.19 -      in
    1.20 -        IsaND.unfix_frees_and_tfrees
    1.21 -          fixes
    1.22 -          (Drule.implies_intr_list
    1.23 -             (Library.gen_distinct
    1.24 -                (fn (x, y) => Thm.term_of x = Thm.term_of y)
    1.25 -                cprems) fixedthconcl)
    1.26 -      end
    1.27 -    else th;
    1.28 -
    1.29 -(* General substiuttion of multiple occurances using one of
    1.30 +(* General substitution of multiple occurances using one of
    1.31     the given theorems*)
    1.32  exception eqsubst_occL_exp of
    1.33            string * (int list) * (thm list) * int * thm;