attribute: Context.mapping;
authorwenzelm
Mon Oct 09 02:19:49 2006 +0200 (2006-10-09)
changeset 208973f8d2834b2c4
parent 20896 1484c7af6d68
child 20898 113c9516a2d7
attribute: Context.mapping;
src/HOL/Import/hol4rews.ML
src/HOL/Import/shuffler.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/arith_data.ML
src/Pure/Proof/extraction.ML
src/Pure/Tools/codegen_data.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Sat Oct 07 07:41:56 2006 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Mon Oct 09 02:19:49 2006 +0200
     1.3 @@ -258,9 +258,8 @@
     1.4  val hol4_debug = ref false
     1.5  fun message s = if !hol4_debug then writeln s else ()
     1.6  
     1.7 -fun add_hol4_rewrite (context, th) =
     1.8 +fun add_hol4_rewrite (Context.Theory thy, th) =
     1.9      let
    1.10 -        val thy = Context.the_theory context;
    1.11  	val _ = message "Adding HOL4 rewrite"
    1.12  	val th1 = th RS eq_reflection
    1.13  	val current_rews = HOL4Rewrites.get thy
    1.14 @@ -268,7 +267,8 @@
    1.15  	val updated_thy  = HOL4Rewrites.put new_rews thy
    1.16      in
    1.17  	(Context.Theory updated_thy,th1)
    1.18 -    end;
    1.19 +    end
    1.20 +  | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
    1.21  
    1.22  fun ignore_hol4 bthy bthm thy =
    1.23      let
     2.1 --- a/src/HOL/Import/shuffler.ML	Sat Oct 07 07:41:56 2006 +0200
     2.2 +++ b/src/HOL/Import/shuffler.ML	Mon Oct 09 02:19:49 2006 +0200
     2.3 @@ -681,7 +681,7 @@
     2.4  	else ShuffleData.put (thm::shuffles) thy
     2.5      end
     2.6  
     2.7 -val shuffle_attr = Thm.declaration_attribute (Context.map_theory o add_shuffle_rule);
     2.8 +val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
     2.9  
    2.10  val setup =
    2.11    Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
     3.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sat Oct 07 07:41:56 2006 +0200
     3.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Oct 09 02:19:49 2006 +0200
     3.3 @@ -47,7 +47,7 @@
     3.4  
     3.5  fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
     3.6  
     3.7 -fun add optmod = Thm.declaration_attribute (fn thm => Context.map_theory (fn thy =>
     3.8 +fun add optmod = Thm.declaration_attribute (fn thm => Context.mapping (fn thy =>
     3.9    let
    3.10      val {intros, graph, eqns} = CodegenData.get thy;
    3.11      fun thyname_of s = (case optmod of
    3.12 @@ -71,7 +71,7 @@
    3.13                 (s, Symtab.lookup_list eqns s @ [(thm, thyname_of s)])} thy
    3.14        | _ => (warn thm; thy))
    3.15      | _ => (warn thm; thy))
    3.16 -  end));
    3.17 +  end) I);
    3.18  
    3.19  fun get_clauses thy s =
    3.20    let val {intros, graph, ...} = CodegenData.get thy
     4.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Oct 07 07:41:56 2006 +0200
     4.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Oct 09 02:19:49 2006 +0200
     4.3 @@ -467,7 +467,7 @@
     4.4      Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
     4.5    end
     4.6  
     4.7 -fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.map_theory
     4.8 +fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
     4.9    let
    4.10      fun err () = error "ind_realizer: bad rule";
    4.11      val sets =
    4.12 @@ -480,7 +480,7 @@
    4.13        (case arg of
    4.14          NONE => sets | SOME NONE => []
    4.15        | SOME (SOME sets') => sets \\ sets')
    4.16 -  end);
    4.17 +  end I);
    4.18  
    4.19  val ind_realizer = Attrib.syntax
    4.20   ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
     5.1 --- a/src/HOL/Tools/recfun_codegen.ML	Sat Oct 07 07:41:56 2006 +0200
     5.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Mon Oct 09 02:19:49 2006 +0200
     5.3 @@ -36,7 +36,7 @@
     5.4  fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
     5.5    string_of_thm thm);
     5.6  
     5.7 -fun add optmod = Thm.declaration_attribute (fn thm => Context.map_theory
     5.8 +fun add optmod = Thm.declaration_attribute (fn thm => Context.mapping
     5.9    let
    5.10      fun add thm =
    5.11        if Pattern.pattern (lhs_of thm) then
    5.12 @@ -47,7 +47,7 @@
    5.13    in
    5.14      add thm
    5.15      #> CodegenData.add_func thm
    5.16 -  end);
    5.17 +  end I);
    5.18  
    5.19  fun del_thm thm thy =
    5.20    let
    5.21 @@ -60,7 +60,7 @@
    5.22    end handle TERM _ => (warn thm; thy);
    5.23  
    5.24  val del = Thm.declaration_attribute
    5.25 -  (fn thm => Context.map_theory (del_thm thm #> CodegenData.del_func thm))
    5.26 +  (fn thm => Context.mapping (del_thm thm #> CodegenData.del_func thm) I)
    5.27  
    5.28  fun del_redundant thy eqs [] = eqs
    5.29    | del_redundant thy eqs (eq :: eqs') =
     6.1 --- a/src/HOL/arith_data.ML	Sat Oct 07 07:41:56 2006 +0200
     6.2 +++ b/src/HOL/arith_data.ML	Mon Oct 09 02:19:49 2006 +0200
     6.3 @@ -231,8 +231,8 @@
     6.4  end);
     6.5  
     6.6  val arith_split_add = Thm.declaration_attribute (fn thm =>
     6.7 -  Context.map_theory (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
     6.8 -    {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics})));
     6.9 +  Context.mapping (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
    6.10 +    {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics})) I);
    6.11  
    6.12  fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
    6.13    {splits = splits, inj_consts = inj_consts, discrete = d :: discrete, tactics= tactics});
     7.1 --- a/src/Pure/Proof/extraction.ML	Sat Oct 07 07:41:56 2006 +0200
     7.2 +++ b/src/Pure/Proof/extraction.ML	Mon Oct 09 02:19:49 2006 +0200
     7.3 @@ -384,7 +384,7 @@
     7.4  val add_expand_thms = fold add_expand_thm;
     7.5  
     7.6  val extraction_expand =
     7.7 -  Attrib.no_args (Thm.declaration_attribute (Context.map_theory o add_expand_thm));
     7.8 +  Attrib.no_args (Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I));
     7.9  
    7.10  
    7.11  (** types with computational content **)
     8.1 --- a/src/Pure/Tools/codegen_data.ML	Sat Oct 07 07:41:56 2006 +0200
     8.2 +++ b/src/Pure/Tools/codegen_data.ML	Mon Oct 09 02:19:49 2006 +0200
     8.3 @@ -837,7 +837,7 @@
     8.4  local
     8.5    fun add_simple_attribute (name, f) =
     8.6      (Codegen.add_attribute name o (Scan.succeed o Thm.declaration_attribute))
     8.7 -      (Context.map_theory o f);
     8.8 +      (fn th => Context.mapping (f th) I);
     8.9  in
    8.10    val _ = map (Context.add_setup o add_simple_attribute) [
    8.11      ("func", add_func),