src/Pure/codegen.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18788 4f4ed2a01152
     1.1 --- a/src/Pure/codegen.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/codegen.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5    val add_codegen: string -> term codegen -> theory -> theory
     1.6    val add_tycodegen: string -> typ codegen -> theory -> theory
     1.7 -  val add_attribute: string -> (Args.T list -> theory attribute * Args.T list) -> theory -> theory
     1.8 +  val add_attribute: string -> (Args.T list -> attribute * Args.T list) -> theory -> theory
     1.9    val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
    1.10    val preprocess: theory -> thm list -> thm list
    1.11    val preprocess_term: theory -> term -> term
    1.12 @@ -207,7 +207,7 @@
    1.13       tycodegens : (string * typ codegen) list,
    1.14       consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
    1.15       types : (string * (typ mixfix list * (string * string) list)) list,
    1.16 -     attrs: (string * (Args.T list -> theory attribute * Args.T list)) list,
    1.17 +     attrs: (string * (Args.T list -> attribute * Args.T list)) list,
    1.18       preprocs: (stamp * (theory -> thm list -> thm list)) list,
    1.19       modules: codegr Symtab.table,
    1.20       test_params: test_params};
    1.21 @@ -312,13 +312,11 @@
    1.22  fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
    1.23  
    1.24  val code_attr =
    1.25 -  Attrib.syntax (Scan.peek (fn thy => foldr op || Scan.fail (map mk_parser
    1.26 -    (#attrs (CodegenData.get thy)))));
    1.27 +  Attrib.syntax (Scan.peek (fn context => foldr op || Scan.fail (map mk_parser
    1.28 +    (#attrs (CodegenData.get (Context.theory_of context))))));
    1.29  
    1.30  val _ = Context.add_setup
    1.31 - (Attrib.add_attributes
    1.32 -  [("code", (code_attr, K Attrib.undef_local_attribute),
    1.33 -     "declare theorems for code generation")]);
    1.34 +  (Attrib.add_attributes [("code", code_attr, "declare theorems for code generation")]);
    1.35  
    1.36  
    1.37  (**** preprocessors ****)
    1.38 @@ -348,10 +346,9 @@
    1.39      | _ => err ()
    1.40    end;
    1.41  
    1.42 -fun unfold_attr (thy, eqn) =
    1.43 +val unfold_attr = Thm.declaration_attribute (fn eqn => Context.map_theory
    1.44    let
    1.45 -    val names = term_consts
    1.46 -      (fst (Logic.dest_equals (prop_of eqn)));
    1.47 +    val names = term_consts (fst (Logic.dest_equals (prop_of eqn)));
    1.48      fun prep thy = map (fn th =>
    1.49        let val prop = prop_of th
    1.50        in
    1.51 @@ -359,7 +356,7 @@
    1.52          then rewrite_rule [eqn] (Thm.transfer thy th)
    1.53          else th
    1.54        end)
    1.55 -  in (add_preprocessor prep thy, eqn) end;
    1.56 +  in add_preprocessor prep end);
    1.57  
    1.58  val _ = Context.add_setup (add_attribute "unfold" (Scan.succeed unfold_attr));
    1.59