src/Pure/codegen.ML
changeset 26463 9283b4185fdf
parent 26455 1757a6e049f4
child 26626 c6231d64d264
     1.1 --- a/src/Pure/codegen.ML	Fri Mar 28 19:43:54 2008 +0100
     1.2 +++ b/src/Pure/codegen.ML	Fri Mar 28 20:02:04 2008 +0100
     1.3 @@ -343,8 +343,8 @@
     1.4    (let
     1.5      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
     1.6    in
     1.7 -    Code.add_attribute ("unfold", Scan.succeed (mk_attribute
     1.8 -      (fn thm => add_unfold thm #> Code.add_inline thm)))
     1.9 +    Context.map_theory (Code.add_attribute ("unfold", Scan.succeed (mk_attribute
    1.10 +      (fn thm => add_unfold thm #> Code.add_inline thm))))
    1.11    end);
    1.12  
    1.13  
    1.14 @@ -786,9 +786,9 @@
    1.15                   (add_edge (node_id, dep) gr'', p module''))
    1.16             end);
    1.17  
    1.18 -val _ = Context.>>
    1.19 +val _ = Context.>> (Context.map_theory
    1.20   (add_codegen "default" default_codegen #>
    1.21 -  add_tycodegen "default" default_tycodegen);
    1.22 +  add_tycodegen "default" default_tycodegen));
    1.23  
    1.24  
    1.25  fun mk_tuple [p] = p
    1.26 @@ -1026,8 +1026,7 @@
    1.27      else state
    1.28    end;
    1.29  
    1.30 -val _ = Context.>>
    1.31 -  (Context.theory_map (Specification.add_theorem_hook test_goal'));
    1.32 +val _ = Context.>> (Specification.add_theorem_hook test_goal');
    1.33  
    1.34  
    1.35  (**** Evaluator for terms ****)
    1.36 @@ -1078,8 +1077,8 @@
    1.37    let val {thy, t, ...} = rep_cterm ct
    1.38    in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
    1.39  
    1.40 -val _ = Context.>>
    1.41 -  (Theory.add_oracle ("evaluation", evaluation_oracle));
    1.42 +val _ = Context.>> (Context.map_theory
    1.43 +  (Theory.add_oracle ("evaluation", evaluation_oracle)));
    1.44  
    1.45  
    1.46  (**** Interface ****)