src/Pure/Isar/object_logic.ML
changeset 12371 80ca9058db95
parent 12311 ce5f9e61c037
child 12479 ed46612ad7ec
     1.1 --- a/src/Pure/Isar/object_logic.ML	Wed Dec 05 03:05:39 2001 +0100
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Wed Dec 05 03:06:05 2001 +0100
     1.3 @@ -111,11 +111,11 @@
     1.4  val get_atomize = #1 o #2 o ObjectLogicData.get_sg;
     1.5  val get_rulify = #2 o #2 o ObjectLogicData.get_sg;
     1.6  
     1.7 -val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules;
     1.8 -val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules;
     1.9 +val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rule;
    1.10 +val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rule;
    1.11  
    1.12 -fun declare_atomize (thy, th) = (add_atomize [th] thy, th);
    1.13 -fun declare_rulify (thy, th) = (add_rulify [th] thy, th);
    1.14 +fun declare_atomize (thy, th) = (add_atomize th thy, th);
    1.15 +fun declare_rulify (thy, th) = (add_rulify th thy, th);
    1.16  
    1.17  
    1.18  (* atomize *)