# HG changeset patch
# User wenzelm
# Date 1535446723 -7200
# Node ID 8207c67d9ef4c66bb96d3e22972718aa03629292
# Parent  7414ce0256e1112e0124b425c4a5e39f38c49d9f
clarified signature: do not expose internal operation;

diff -r 7414ce0256e1 -r 8207c67d9ef4 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Mon Aug 27 22:58:36 2018 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Aug 28 10:58:43 2018 +0200
@@ -1490,7 +1490,7 @@
 ML \<open>
 fun remove_duplicates_tac feats =
   (if can_feature (CleanUp [RemoveDuplicates]) feats then
-     ALLGOALS distinct_subgoal_tac
+     distinct_subgoals_tac
    else all_tac)
 \<close>
 
diff -r 7414ce0256e1 -r 8207c67d9ef4 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Aug 27 22:58:36 2018 +0200
+++ b/src/Pure/tactic.ML	Tue Aug 28 10:58:43 2018 +0200
@@ -28,7 +28,6 @@
   val ematch_tac: Proof.context -> thm list -> int -> tactic
   val dmatch_tac: Proof.context -> thm list -> int -> tactic
   val flexflex_tac: Proof.context -> tactic
-  val distinct_subgoal_tac: int -> tactic
   val distinct_subgoals_tac: tactic
   val cut_tac: thm -> int -> tactic
   val cut_rules_tac: thm list -> int -> tactic