src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
changeset 54006 9fe1bd54d437
parent 53920 c6de7f20c845
     1.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Tue Oct 01 12:53:24 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Tue Oct 01 14:05:25 2013 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  Tactics for wrapping existing freely generated type's constructors.
     1.5  *)
     1.6  
     1.7 -signature BNF_CTR_SUGAR_TACTICS =
     1.8 +signature CTR_SUGAR_TACTICS =
     1.9  sig
    1.10    val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
    1.11    val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
    1.12 @@ -26,7 +26,7 @@
    1.13    val mk_unique_disc_def_tac: int -> thm -> tactic
    1.14  end;
    1.15  
    1.16 -structure BNF_Ctr_Sugar_Tactics : BNF_CTR_SUGAR_TACTICS =
    1.17 +structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS =
    1.18  struct
    1.19  
    1.20  open BNF_Util