src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 68825 8207c67d9ef4
parent 67613 ce654b0e6d69
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Mon Aug 27 22:58:36 2018 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Aug 28 10:58:43 2018 +0200
     1.3 @@ -1490,7 +1490,7 @@
     1.4  ML \<open>
     1.5  fun remove_duplicates_tac feats =
     1.6    (if can_feature (CleanUp [RemoveDuplicates]) feats then
     1.7 -     ALLGOALS distinct_subgoal_tac
     1.8 +     distinct_subgoals_tac
     1.9     else all_tac)
    1.10  \<close>
    1.11