# HG changeset patch # User wenzelm # Date 1140035697 -3600 # Node ID 670ce193b6182f7088863fe364ab98df74a6ff30 # Parent bc5c6c9b114e8036b9c6c665b96a15d887e5c68c used Tactic.distinct_subgoals_tac; diff -r bc5c6c9b114e -r 670ce193b618 src/Provers/eqsubst.ML --- a/src/Provers/eqsubst.ML Wed Feb 15 21:34:55 2006 +0100 +++ b/src/Provers/eqsubst.ML Wed Feb 15 21:34:57 2006 +0100 @@ -146,26 +146,11 @@ in stepthms |> Seq.maps rewrite_with_thm end; -(* Tactic.distinct_subgoals_tac -- fails to free type variables *) - -(* custom version of distinct subgoals that works with term and - type variables. Asssumes th is in beta-eta normal form. - Also, does nothing if flexflex contraints are present. *) +(* distinct subgoals *) fun distinct_subgoals th = - if List.null (Thm.tpairs_of th) then - let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th - val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm - in - IsaND.unfix_frees_and_tfrees - fixes - (Drule.implies_intr_list - (Library.gen_distinct - (fn (x, y) => Thm.term_of x = Thm.term_of y) - cprems) fixedthconcl) - end - else th; + the_default th (SINGLE distinct_subgoals_tac th); -(* General substiuttion of multiple occurances using one of +(* General substitution of multiple occurances using one of the given theorems*) exception eqsubst_occL_exp of string * (int list) * (thm list) * int * thm;