src/Pure/Isar/calculation.ML
changeset 26463 9283b4185fdf
parent 26435 bdce320cd426
child 28210 c164d1892553
     1.1 --- a/src/Pure/Isar/calculation.ML	Fri Mar 28 19:43:54 2008 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Fri Mar 28 20:02:04 2008 +0100
     1.3 @@ -92,14 +92,14 @@
     1.4  val trans_att = Attrib.add_del_args trans_add trans_del;
     1.5  val sym_att = Attrib.add_del_args sym_add sym_del;
     1.6  
     1.7 -val _ = Context.>>
     1.8 +val _ = Context.>> (Context.map_theory
     1.9   (Attrib.add_attributes
    1.10     [("trans", trans_att, "declaration of transitivity rule"),
    1.11      ("sym", sym_att, "declaration of symmetry rule"),
    1.12      ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
    1.13    PureThy.add_thms
    1.14     [(("", transitive_thm), [trans_add]),
    1.15 -    (("", symmetric_thm), [sym_add])] #> snd);
    1.16 +    (("", symmetric_thm), [sym_add])] #> snd));
    1.17  
    1.18  
    1.19