# HG changeset patch
# User wenzelm
# Date 1538404896 -7200
# Node ID 991a3feaf2700b09dc600d781814b8d74c8f7f00
# Parent  0b0c3dfd730f27aa358d10efd50807f5db43c106
more direct implementation of distinct_subgoals_tac -- potentially more efficient;

diff -r 0b0c3dfd730f -r 991a3feaf270 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Oct 01 16:40:45 2018 +0200
+++ b/src/Pure/tactic.ML	Mon Oct 01 16:41:36 2018 +0200
@@ -144,26 +144,37 @@
 fun flexflex_tac ctxt = PRIMSEQ (Thm.flexflex_rule (SOME ctxt));
 
 (*Remove duplicate subgoals.*)
-val permute_tac = PRIMITIVE oo Thm.permute_prems;
-fun distinct_tac (i, k) =
-  permute_tac 0 (i - 1) THEN
-  permute_tac 1 (k - 1) THEN
-  PRIMITIVE (fn st => Drule.comp_no_flatten (st, 0) 1 Drule.distinct_prems_rl) THEN
-  permute_tac 1 (1 - k) THEN
-  permute_tac 0 (1 - i);
+fun distinct_subgoals_tac st =
+  let
+    val subgoals = Thm.cprems_of st;
+    val (tab, n) =
+      (subgoals, (Ctermtab.empty, 0)) |-> fold (fn ct => fn (tab, i) =>
+        if Ctermtab.defined tab ct then (tab, i)
+        else (Ctermtab.update (ct, i) tab, i + 1));
+    val st' =
+      if n = length subgoals then st
+      else
+        let
+          val thy = Thm.theory_of_thm st;
+          fun cert_prop i = Thm.global_cterm_of thy (Free (Name.bound i, propT));
 
-fun distinct_subgoal_tac i st =
-  (case drop (i - 1) (Thm.prems_of st) of
-    [] => no_tac st
-  | A :: Bs =>
-      st |> EVERY (fold (fn (B, k) =>
-        if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) []));
+          val As = map (cert_prop o the o Ctermtab.lookup tab) subgoals;
+          val As' = map cert_prop (0 upto (n - 1));
+          val C = cert_prop n;
 
-fun distinct_subgoals_tac state =
-  let
-    val goals = Thm.prems_of state;
-    val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals));
-  in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end;
+          val template = Drule.list_implies (As, C);
+          val inst =
+            (dest_Free (Thm.term_of C), Thm.cconcl_of st) ::
+              Ctermtab.fold (fn (ct, i) => cons ((Name.bound i, propT), ct)) tab [];
+        in
+          Thm.assume template
+          |> fold (Thm.elim_implies o Thm.assume) As
+          |> fold_rev Thm.implies_intr As'
+          |> Thm.implies_intr template
+          |> Thm.instantiate_frees ([], inst)
+          |> Thm.elim_implies st
+        end;
+  in Seq.single st' end;
 
 
 (*** Applications of cut_rl ***)
diff -r 0b0c3dfd730f -r 991a3feaf270 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Oct 01 16:40:45 2018 +0200
+++ b/src/Pure/thm.ML	Mon Oct 01 16:41:36 2018 +0200
@@ -71,6 +71,8 @@
   val major_prem_of: thm -> term
   val cprop_of: thm -> cterm
   val cprem_of: thm -> int -> cterm
+  val cconcl_of: thm -> cterm
+  val cprems_of: thm -> cterm list
   val chyps_of: thm -> cterm list
   exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option
   val theory_of_cterm: cterm -> theory
@@ -397,6 +399,13 @@
   Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps,
     t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])};
 
+fun cconcl_of (th as Thm (_, {cert, maxidx, shyps, ...})) =
+  Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = concl_of th};
+
+fun cprems_of (th as Thm (_, {cert, maxidx, shyps, ...})) =
+  map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t})
+    (prems_of th);
+
 fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) =
   map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;