src/Pure/Isar/code.ML
changeset 26435 bdce320cd426
parent 26021 25d06476727e
child 26463 9283b4185fdf
     1.1 --- a/src/Pure/Isar/code.ML	Thu Mar 27 15:32:12 2008 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Mar 27 15:32:15 2008 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4      val code_attr = Attrib.syntax (Scan.peek (fn context =>
     1.5        List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
     1.6    in
     1.7 -    Context.add_setup (Attrib.add_attributes
     1.8 +    Context.>> (Attrib.add_attributes
     1.9        [("code", code_attr, "declare theorems for code generation")])
    1.10    end;
    1.11  
    1.12 @@ -387,7 +387,7 @@
    1.13      in (exec, ref data) end;
    1.14  );
    1.15  
    1.16 -val _ = Context.add_setup CodeData.init;
    1.17 +val _ = Context.>> CodeData.init;
    1.18  
    1.19  fun thy_data f thy = f ((snd o CodeData.get) thy);
    1.20  
    1.21 @@ -864,7 +864,7 @@
    1.22      (remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
    1.23          (*fully applied in order to get right context for mk_rew!*)
    1.24  
    1.25 -val _ = Context.add_setup
    1.26 +val _ = Context.>>
    1.27    (let
    1.28      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    1.29      fun add_simple_attribute (name, f) =