src/HOL/Tools/recdef_package.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18799 f137c5e971f5
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -11,24 +11,23 @@
     1.4    val print_recdefs: theory -> unit
     1.5    val get_recdef: theory -> string
     1.6      -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
     1.7 -  val simp_add: Context.generic attribute
     1.8 -  val simp_del: Context.generic attribute
     1.9 -  val cong_add: Context.generic attribute
    1.10 -  val cong_del: Context.generic attribute
    1.11 -  val wf_add: Context.generic attribute
    1.12 -  val wf_del: Context.generic attribute
    1.13 +  val simp_add: attribute
    1.14 +  val simp_del: attribute
    1.15 +  val cong_add: attribute
    1.16 +  val cong_del: attribute
    1.17 +  val wf_add: attribute
    1.18 +  val wf_del: attribute
    1.19    val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
    1.20      Attrib.src option -> theory -> theory
    1.21        * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    1.22 -  val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * theory attribute list) list ->
    1.23 +  val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list ->
    1.24      theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    1.25    val defer_recdef: xstring -> string list -> (thmref * Attrib.src list) list
    1.26      -> theory -> theory * {induct_rules: thm}
    1.27 -  val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list
    1.28 +  val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list
    1.29      -> theory -> theory * {induct_rules: thm}
    1.30    val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> theory -> Proof.state
    1.31 -  val recdef_tc_i: bstring * theory attribute list -> string -> int option
    1.32 -    -> theory -> Proof.state
    1.33 +  val recdef_tc_i: bstring * attribute list -> string -> int option -> theory -> Proof.state
    1.34    val setup: theory -> theory
    1.35  end;
    1.36  
    1.37 @@ -148,7 +147,7 @@
    1.38  fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy)
    1.39    | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt);
    1.40  
    1.41 -fun attrib f = Attrib.declaration (map_hints o f);
    1.42 +fun attrib f = Thm.declaration_attribute (map_hints o f);
    1.43  
    1.44  val simp_add = attrib (map_simps o Drule.add_rule);
    1.45  val simp_del = attrib (map_simps o Drule.del_rule);
    1.46 @@ -165,15 +164,15 @@
    1.47  val recdef_wfN = "recdef_wf";
    1.48  
    1.49  val recdef_modifiers =
    1.50 - [Args.$$$ recdef_simpN -- Args.colon >> K ((I, Attrib.context simp_add): Method.modifier),
    1.51 -  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
    1.52 -  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
    1.53 -  Args.$$$ recdef_congN -- Args.colon >> K (I, Attrib.context cong_add),
    1.54 -  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
    1.55 -  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del),
    1.56 -  Args.$$$ recdef_wfN -- Args.colon >> K (I, Attrib.context wf_add),
    1.57 -  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, Attrib.context wf_add),
    1.58 -  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, Attrib.context wf_del)] @
    1.59 + [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add): Method.modifier),
    1.60 +  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add),
    1.61 +  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del),
    1.62 +  Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add),
    1.63 +  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add),
    1.64 +  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del),
    1.65 +  Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add),
    1.66 +  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add),
    1.67 +  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del)] @
    1.68    Clasimp.clasimp_modifiers;
    1.69  
    1.70  
    1.71 @@ -223,8 +222,7 @@
    1.72          tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
    1.73                 congs wfs name R eqs;
    1.74      val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
    1.75 -    val simp_att = if null tcs then
    1.76 -      [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE] else [];
    1.77 +    val simp_att = if null tcs then [Simplifier.simp_add, RecfunCodegen.add NONE] else [];
    1.78  
    1.79      val ((simps' :: rules', [induct']), thy) =
    1.80        thy
    1.81 @@ -239,7 +237,7 @@
    1.82        |> Theory.parent_path;
    1.83    in (thy, result) end;
    1.84  
    1.85 -val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints;
    1.86 +val add_recdef = gen_add_recdef Tfl.define Attrib.attribute prepare_hints;
    1.87  fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
    1.88  
    1.89  
    1.90 @@ -284,7 +282,7 @@
    1.91          " in recdef definition of " ^ quote name);
    1.92    in IsarThy.theorem_i Drule.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
    1.93  
    1.94 -val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const;
    1.95 +val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const;
    1.96  val recdef_tc_i = gen_recdef_tc (K I) (K I);
    1.97  
    1.98  
    1.99 @@ -297,12 +295,9 @@
   1.100    GlobalRecdefData.init #>
   1.101    LocalRecdefData.init #>
   1.102    Attrib.add_attributes
   1.103 -   [(recdef_simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
   1.104 -      "declaration of recdef simp rule"),
   1.105 -    (recdef_congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
   1.106 -      "declaration of recdef cong rule"),
   1.107 -    (recdef_wfN, Attrib.common (Attrib.add_del_args wf_add wf_del),
   1.108 -      "declaration of recdef wf rule")];
   1.109 +   [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
   1.110 +    (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
   1.111 +    (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];
   1.112  
   1.113  
   1.114  (* outer syntax *)