1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Wed Jun 03 09:56:24 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Wed Jun 03 11:25:19 2020 +0200
     1.3 @@ -269,9 +269,9 @@
     1.4    | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
     1.5    | try_rew _ _ _ _ _ _ = raise ERROR "try_rew: uncovered case"
     1.6  and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) = 
     1.7 -    gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
     1.8 +    distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
     1.9    | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) = 
    1.10 -    gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
    1.11 +    distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
    1.12    | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
    1.13    | filter_appl_rews _ _ _ _ = raise ERROR "filter_appl_rews: uncovered case"
    1.14