src/Pure/Isar/object_logic.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18783 628e57610536
     1.1 --- a/src/Pure/Isar/object_logic.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -14,8 +14,8 @@
     1.4    val drop_judgment: theory -> term -> term
     1.5    val fixed_judgment: theory -> string -> term
     1.6    val ensure_propT: theory -> term -> term
     1.7 -  val declare_atomize: theory attribute
     1.8 -  val declare_rulify: theory attribute
     1.9 +  val declare_atomize: attribute
    1.10 +  val declare_rulify: attribute
    1.11    val atomize_term: theory -> term -> term
    1.12    val atomize_cterm: theory -> cterm -> thm
    1.13    val atomize_thm: thm -> thm
    1.14 @@ -24,8 +24,8 @@
    1.15    val atomize_goal: int -> thm -> thm
    1.16    val rulify: thm -> thm
    1.17    val rulify_no_asm: thm -> thm
    1.18 -  val rule_format: 'a attribute
    1.19 -  val rule_format_no_asm: 'a attribute
    1.20 +  val rule_format: attribute
    1.21 +  val rule_format_no_asm: attribute
    1.22  end;
    1.23  
    1.24  structure ObjectLogic: OBJECT_LOGIC =
    1.25 @@ -123,11 +123,13 @@
    1.26  val get_atomize = #1 o #2 o ObjectLogicData.get;
    1.27  val get_rulify = #2 o #2 o ObjectLogicData.get;
    1.28  
    1.29 -val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rule;
    1.30 -val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rule;
    1.31 +val declare_atomize =
    1.32 +  Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o
    1.33 +    Library.apsnd o Library.apfst o Drule.add_rule);
    1.34  
    1.35 -fun declare_atomize (thy, th) = (add_atomize th thy, th);
    1.36 -fun declare_rulify (thy, th) = (add_rulify th thy, th);
    1.37 +val declare_rulify =
    1.38 +  Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o
    1.39 +    Library.apsnd o Library.apsnd o Drule.add_rule);
    1.40  
    1.41  
    1.42  (* atomize *)
    1.43 @@ -164,8 +166,8 @@
    1.44  val rulify = gen_rulify true;
    1.45  val rulify_no_asm = gen_rulify false;
    1.46  
    1.47 -fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
    1.48 -fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
    1.49 +fun rule_format x = Thm.rule_attribute (fn _ => rulify) x;
    1.50 +fun rule_format_no_asm x = Thm.rule_attribute (fn _ => rulify_no_asm) x;
    1.51  
    1.52  
    1.53  end;