src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 49543 53b3c532a082
parent 49542 b39354db8629
child 49544 24094fa47e0d
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -59,7 +59,7 @@
     thm list list -> thm list list list -> tactic
   val mk_map_id_tac: thm list -> thm -> thm -> tactic
   val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
-  val mk_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
   val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
   val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list ->
     thm list -> {prems: 'a, context: Proof.context} -> tactic
@@ -1255,7 +1255,7 @@
            rtac conjI, rtac refl, rtac refl]) ks]) 1
   end
 
-fun mk_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
+fun mk_dtor_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
   rtac unfold_unique 1 THEN
   unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
   ALLGOALS (etac sym);