diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Mar 27 15:32:12 2008 +0100 +++ b/src/Pure/Isar/code.ML Thu Mar 27 15:32:15 2008 +0100 @@ -107,7 +107,7 @@ val code_attr = Attrib.syntax (Scan.peek (fn context => List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context))))); in - Context.add_setup (Attrib.add_attributes + Context.>> (Attrib.add_attributes [("code", code_attr, "declare theorems for code generation")]) end; @@ -387,7 +387,7 @@ in (exec, ref data) end; ); -val _ = Context.add_setup CodeData.init; +val _ = Context.>> CodeData.init; fun thy_data f thy = f ((snd o CodeData.get) thy); @@ -864,7 +864,7 @@ (remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy; (*fully applied in order to get right context for mk_rew!*) -val _ = Context.add_setup +val _ = Context.>> (let fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); fun add_simple_attribute (name, f) =