# HG changeset patch
# User wenzelm
# Date 1319814952 -7200
# Node ID f599ac41e7f57dcf4f4517a4e049b0d44d44976b
# Parent  25e9e7f527b48704ac6e4233709f634d225b02dc
tuned signature -- refined terminology;

diff -r 25e9e7f527b4 -r f599ac41e7f5 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/HOL/Tools/Function/function.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -128,7 +128,7 @@
         val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
       in
         (info,
-         lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
+         lthy |> Local_Theory.declaration false (add_function_data o transform_function_data info))
       end
   in
     ((goal_state, afterqed), lthy')
@@ -203,7 +203,7 @@
             in
               (info',
                lthy 
-               |> Local_Theory.declaration false (add_function_data o morph_function_data info')
+               |> Local_Theory.declaration false (add_function_data o transform_function_data info')
                |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
             end)
         end
diff -r 25e9e7f527b4 -r f599ac41e7f5 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -93,10 +93,12 @@
   termination : thm,
   domintros : thm list option}
 
-fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
+fun transform_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
   simps, inducts, termination, defname, is_partial} : info) phi =
     let
-      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
+      val term = Morphism.term phi
+      val thm = Morphism.thm phi
+      val fact = Morphism.fact phi
       val name = Binding.name_of o Morphism.binding phi o Binding.name
     in
       { add_simps = add_simps, case_names = case_names,
@@ -132,7 +134,7 @@
     val inst_morph = lift_morphism thy o Thm.instantiate
 
     fun match (trm, data) =
-      SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
+      SOME (transform_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
       handle Pattern.MATCH => NONE
   in
     get_first match (Item_Net.retrieve (get_function ctxt) t)
diff -r 25e9e7f527b4 -r f599ac41e7f5 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -23,7 +23,7 @@
   type inductive_result =
     {preds: term list, elims: thm list, raw_induct: thm,
      induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}
-  val morph_result: morphism -> inductive_result -> inductive_result
+  val transform_result: morphism -> inductive_result -> inductive_result
   type inductive_info = {names: string list, coind: bool} * inductive_result
   val the_inductive: Proof.context -> string -> inductive_info
   val print_inductives: Proof.context -> unit
@@ -120,7 +120,7 @@
   {preds: term list, elims: thm list, raw_induct: thm,
    induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
 
-fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
+fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
   let
     val term = Morphism.term phi;
     val thm = Morphism.thm phi;
@@ -932,7 +932,7 @@
 
     val lthy4 = lthy3
       |> Local_Theory.declaration false (fn phi =>
-        let val result' = morph_result phi result;
+        let val result' = transform_result phi result;
         in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
   in (result, lthy4) end;
 
diff -r 25e9e7f527b4 -r f599ac41e7f5 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/Pure/Isar/args.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -12,7 +12,7 @@
   val dest_src: src -> (string * Token.T list) * Position.T
   val pretty_src: Proof.context -> src -> Pretty.T
   val map_name: (string -> string) -> src -> src
-  val morph_values: morphism -> src -> src
+  val transform_values: morphism -> src -> src
   val assignable: src -> src
   val closure: src -> src
   val context: Proof.context context_parser
@@ -96,7 +96,7 @@
 
 (* values *)
 
-fun morph_values phi = map_args (Token.map_value
+fun transform_values phi = map_args (Token.map_value
   (fn Token.Text s => Token.Text s
     | Token.Typ T => Token.Typ (Morphism.typ phi T)
     | Token.Term t => Token.Term (Morphism.term phi t)
diff -r 25e9e7f527b4 -r f599ac41e7f5 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/Pure/Isar/element.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -28,7 +28,7 @@
     ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
   val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
     ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
-  val morph_ctxt: morphism -> context_i -> context_i
+  val transform_ctxt: morphism -> context_i -> context_i
   val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
   val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
   val pretty_statement: Proof.context -> string -> thm -> Pretty.T
@@ -43,7 +43,7 @@
   val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) ->
     string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
     Proof.state
-  val morph_witness: morphism -> witness -> witness
+  val transform_witness: morphism -> witness -> witness
   val conclude_witness: witness -> thm
   val pretty_witness: Proof.context -> witness -> Pretty.T
   val instT_type: typ Symtab.table -> typ -> typ
@@ -110,13 +110,13 @@
 fun map_ctxt_attrib attrib =
   map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib};
 
-fun morph_ctxt phi = map_ctxt
+fun transform_ctxt phi = map_ctxt
  {binding = Morphism.binding phi,
   typ = Morphism.typ phi,
   term = Morphism.term phi,
   pattern = Morphism.term phi,
   fact = Morphism.fact phi,
-  attrib = Args.morph_values phi};
+  attrib = Args.transform_values phi};
 
 
 
@@ -269,7 +269,7 @@
 fun witness_hyps (Witness (_, th)) = Thm.hyps_of th;
 fun map_witness f (Witness witn) = Witness (f witn);
 
-fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
+fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
 
 fun prove_witness ctxt t tac =
   Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ =>
@@ -461,7 +461,7 @@
     | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
 
 val satisfy_morphism = Morphism.thm_morphism o satisfy_thm;
-val satisfy_facts = facts_map o morph_ctxt o satisfy_morphism;
+val satisfy_facts = facts_map o transform_ctxt o satisfy_morphism;
 
 
 (* rewriting with equalities *)
diff -r 25e9e7f527b4 -r f599ac41e7f5 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -771,10 +771,10 @@
 
     val notes' = body_elems |>
       map (defines_to_notes thy') |>
-      map (Element.morph_ctxt a_satisfy) |>
+      map (Element.transform_ctxt a_satisfy) |>
       (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
       fst |>
-      map (Element.morph_ctxt b_satisfy) |>
+      map (Element.transform_ctxt b_satisfy) |>
       map_filter (fn Notes notes => SOME notes | _ => NONE);
 
     val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
@@ -823,7 +823,7 @@
     |-> (fn eqns => fold (fn ((dep, morph), wits) =>
       fn context =>
         Locale.add_registration (dep, morph $> Element.satisfy_morphism
-            (map (Element.morph_witness export') wits))
+            (map (Element.transform_witness export') wits))
           (Element.eq_morphism (Context.theory_of context) eqns |>
             Option.map (rpair true))
           export context) (deps ~~ witss))
@@ -902,7 +902,7 @@
       fn theory =>
         Locale.add_dependency target
           (dep, morph $> Element.satisfy_morphism
-            (map (Element.morph_witness export') wits))
+            (map (Element.transform_witness export') wits))
           (Element.eq_morphism theory eqns' |> Option.map (rpair true))
           export theory) (deps ~~ witss))
   end;
diff -r 25e9e7f527b4 -r f599ac41e7f5 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -425,7 +425,7 @@
             NONE => Morphism.identity
           | SOME export => collect_mixins context (name, morph $> export) $> export);
         val facts' = facts
-          |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin));
+          |> Element.facts_map (Element.transform_ctxt (transfer input $> morph $> mixin));
       in activ_elem (Notes (kind, facts')) input end;
   in
     fold_rev activate notes input
@@ -562,7 +562,7 @@
       (* Registrations *)
       (fn thy => fold_rev (fn (_, morph) =>
             let
-              val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
+              val args'' = snd args' |> Element.facts_map (Element.transform_ctxt morph) |>
                 Attrib.map_facts (Attrib.attribute_i thy)
             in Global_Theory.note_thmss kind args'' #> snd end)
         (registrations_of (Context.Theory thy) loc) thy))
diff -r 25e9e7f527b4 -r f599ac41e7f5 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/Pure/Isar/named_target.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -118,7 +118,7 @@
   let
     val global_facts' = Attrib.map_facts (K I) global_facts;
     val local_facts' = Element.facts_map
-      (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
+      (Element.transform_ctxt (Local_Theory.target_morphism lthy)) local_facts;
   in
     lthy
     |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
diff -r 25e9e7f527b4 -r f599ac41e7f5 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/Pure/raw_simplifier.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -33,7 +33,7 @@
     safe_solvers: string list}
   type simproc
   val eq_simproc: simproc * simproc -> bool
-  val morph_simproc: morphism -> simproc -> simproc
+  val transform_simproc: morphism -> simproc -> simproc
   val make_simproc: {name: string, lhss: cterm list,
     proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
   val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
@@ -625,7 +625,7 @@
 
 fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
 
-fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
+fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
   Simproc
    {name = name,
     lhss = map (Morphism.cterm phi) lhss,
diff -r 25e9e7f527b4 -r f599ac41e7f5 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/Pure/simplifier.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -195,7 +195,7 @@
     lthy |> Local_Theory.declaration false (fn phi => fn context =>
       let
         val b' = Morphism.binding phi b;
-        val simproc' = morph_simproc phi simproc;
+        val simproc' = transform_simproc phi simproc;
       in
         context
         |> Data.map (fn (ss, tab) =>
@@ -298,7 +298,7 @@
   (Args.del -- Args.colon >> K (op delsimprocs) ||
     Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
   >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
-      (K (map_ss (fn ss => f (ss, [morph_simproc phi simproc])))));
+      (K (map_ss (fn ss => f (ss, [transform_simproc phi simproc])))));
 
 in
 
diff -r 25e9e7f527b4 -r f599ac41e7f5 src/Tools/interpretation_with_defs.ML
--- a/src/Tools/interpretation_with_defs.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/Tools/interpretation_with_defs.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -30,7 +30,7 @@
     |-> (fn eqns => fold (fn ((dep, morph), wits) =>
       fn context =>
         Locale.add_registration (dep, morph $> Element.satisfy_morphism
-            (map (Element.morph_witness export') wits))
+            (map (Element.transform_witness export') wits))
           (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
             Option.map (rpair true))
           export context) (deps ~~ witss))