1.1 --- a/src/HOL/Tools/Function/function.ML Fri Oct 28 15:38:41 2011 +0200
1.2 +++ b/src/HOL/Tools/Function/function.ML Fri Oct 28 17:15:52 2011 +0200
1.3 @@ -128,7 +128,7 @@
1.4 val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
1.5 in
1.6 (info,
1.7 - lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
1.8 + lthy |> Local_Theory.declaration false (add_function_data o transform_function_data info))
1.9 end
1.10 in
1.11 ((goal_state, afterqed), lthy')
1.12 @@ -203,7 +203,7 @@
1.13 in
1.14 (info',
1.15 lthy
1.16 - |> Local_Theory.declaration false (add_function_data o morph_function_data info')
1.17 + |> Local_Theory.declaration false (add_function_data o transform_function_data info')
1.18 |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
1.19 end)
1.20 end
2.1 --- a/src/HOL/Tools/Function/function_common.ML Fri Oct 28 15:38:41 2011 +0200
2.2 +++ b/src/HOL/Tools/Function/function_common.ML Fri Oct 28 17:15:52 2011 +0200
2.3 @@ -93,10 +93,12 @@
2.4 termination : thm,
2.5 domintros : thm list option}
2.6
2.7 -fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
2.8 +fun transform_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
2.9 simps, inducts, termination, defname, is_partial} : info) phi =
2.10 let
2.11 - val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
2.12 + val term = Morphism.term phi
2.13 + val thm = Morphism.thm phi
2.14 + val fact = Morphism.fact phi
2.15 val name = Binding.name_of o Morphism.binding phi o Binding.name
2.16 in
2.17 { add_simps = add_simps, case_names = case_names,
2.18 @@ -132,7 +134,7 @@
2.19 val inst_morph = lift_morphism thy o Thm.instantiate
2.20
2.21 fun match (trm, data) =
2.22 - SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
2.23 + SOME (transform_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
2.24 handle Pattern.MATCH => NONE
2.25 in
2.26 get_first match (Item_Net.retrieve (get_function ctxt) t)
3.1 --- a/src/HOL/Tools/inductive.ML Fri Oct 28 15:38:41 2011 +0200
3.2 +++ b/src/HOL/Tools/inductive.ML Fri Oct 28 17:15:52 2011 +0200
3.3 @@ -23,7 +23,7 @@
3.4 type inductive_result =
3.5 {preds: term list, elims: thm list, raw_induct: thm,
3.6 induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}
3.7 - val morph_result: morphism -> inductive_result -> inductive_result
3.8 + val transform_result: morphism -> inductive_result -> inductive_result
3.9 type inductive_info = {names: string list, coind: bool} * inductive_result
3.10 val the_inductive: Proof.context -> string -> inductive_info
3.11 val print_inductives: Proof.context -> unit
3.12 @@ -120,7 +120,7 @@
3.13 {preds: term list, elims: thm list, raw_induct: thm,
3.14 induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
3.15
3.16 -fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
3.17 +fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
3.18 let
3.19 val term = Morphism.term phi;
3.20 val thm = Morphism.thm phi;
3.21 @@ -932,7 +932,7 @@
3.22
3.23 val lthy4 = lthy3
3.24 |> Local_Theory.declaration false (fn phi =>
3.25 - let val result' = morph_result phi result;
3.26 + let val result' = transform_result phi result;
3.27 in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
3.28 in (result, lthy4) end;
3.29
4.1 --- a/src/Pure/Isar/args.ML Fri Oct 28 15:38:41 2011 +0200
4.2 +++ b/src/Pure/Isar/args.ML Fri Oct 28 17:15:52 2011 +0200
4.3 @@ -12,7 +12,7 @@
4.4 val dest_src: src -> (string * Token.T list) * Position.T
4.5 val pretty_src: Proof.context -> src -> Pretty.T
4.6 val map_name: (string -> string) -> src -> src
4.7 - val morph_values: morphism -> src -> src
4.8 + val transform_values: morphism -> src -> src
4.9 val assignable: src -> src
4.10 val closure: src -> src
4.11 val context: Proof.context context_parser
4.12 @@ -96,7 +96,7 @@
4.13
4.14 (* values *)
4.15
4.16 -fun morph_values phi = map_args (Token.map_value
4.17 +fun transform_values phi = map_args (Token.map_value
4.18 (fn Token.Text s => Token.Text s
4.19 | Token.Typ T => Token.Typ (Morphism.typ phi T)
4.20 | Token.Term t => Token.Term (Morphism.term phi t)
5.1 --- a/src/Pure/Isar/element.ML Fri Oct 28 15:38:41 2011 +0200
5.2 +++ b/src/Pure/Isar/element.ML Fri Oct 28 17:15:52 2011 +0200
5.3 @@ -28,7 +28,7 @@
5.4 ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
5.5 val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
5.6 ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
5.7 - val morph_ctxt: morphism -> context_i -> context_i
5.8 + val transform_ctxt: morphism -> context_i -> context_i
5.9 val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
5.10 val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
5.11 val pretty_statement: Proof.context -> string -> thm -> Pretty.T
5.12 @@ -43,7 +43,7 @@
5.13 val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) ->
5.14 string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
5.15 Proof.state
5.16 - val morph_witness: morphism -> witness -> witness
5.17 + val transform_witness: morphism -> witness -> witness
5.18 val conclude_witness: witness -> thm
5.19 val pretty_witness: Proof.context -> witness -> Pretty.T
5.20 val instT_type: typ Symtab.table -> typ -> typ
5.21 @@ -110,13 +110,13 @@
5.22 fun map_ctxt_attrib attrib =
5.23 map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib};
5.24
5.25 -fun morph_ctxt phi = map_ctxt
5.26 +fun transform_ctxt phi = map_ctxt
5.27 {binding = Morphism.binding phi,
5.28 typ = Morphism.typ phi,
5.29 term = Morphism.term phi,
5.30 pattern = Morphism.term phi,
5.31 fact = Morphism.fact phi,
5.32 - attrib = Args.morph_values phi};
5.33 + attrib = Args.transform_values phi};
5.34
5.35
5.36
5.37 @@ -269,7 +269,7 @@
5.38 fun witness_hyps (Witness (_, th)) = Thm.hyps_of th;
5.39 fun map_witness f (Witness witn) = Witness (f witn);
5.40
5.41 -fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
5.42 +fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
5.43
5.44 fun prove_witness ctxt t tac =
5.45 Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ =>
5.46 @@ -461,7 +461,7 @@
5.47 | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
5.48
5.49 val satisfy_morphism = Morphism.thm_morphism o satisfy_thm;
5.50 -val satisfy_facts = facts_map o morph_ctxt o satisfy_morphism;
5.51 +val satisfy_facts = facts_map o transform_ctxt o satisfy_morphism;
5.52
5.53
5.54 (* rewriting with equalities *)
6.1 --- a/src/Pure/Isar/expression.ML Fri Oct 28 15:38:41 2011 +0200
6.2 +++ b/src/Pure/Isar/expression.ML Fri Oct 28 17:15:52 2011 +0200
6.3 @@ -771,10 +771,10 @@
6.4
6.5 val notes' = body_elems |>
6.6 map (defines_to_notes thy') |>
6.7 - map (Element.morph_ctxt a_satisfy) |>
6.8 + map (Element.transform_ctxt a_satisfy) |>
6.9 (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
6.10 fst |>
6.11 - map (Element.morph_ctxt b_satisfy) |>
6.12 + map (Element.transform_ctxt b_satisfy) |>
6.13 map_filter (fn Notes notes => SOME notes | _ => NONE);
6.14
6.15 val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
6.16 @@ -823,7 +823,7 @@
6.17 |-> (fn eqns => fold (fn ((dep, morph), wits) =>
6.18 fn context =>
6.19 Locale.add_registration (dep, morph $> Element.satisfy_morphism
6.20 - (map (Element.morph_witness export') wits))
6.21 + (map (Element.transform_witness export') wits))
6.22 (Element.eq_morphism (Context.theory_of context) eqns |>
6.23 Option.map (rpair true))
6.24 export context) (deps ~~ witss))
6.25 @@ -902,7 +902,7 @@
6.26 fn theory =>
6.27 Locale.add_dependency target
6.28 (dep, morph $> Element.satisfy_morphism
6.29 - (map (Element.morph_witness export') wits))
6.30 + (map (Element.transform_witness export') wits))
6.31 (Element.eq_morphism theory eqns' |> Option.map (rpair true))
6.32 export theory) (deps ~~ witss))
6.33 end;
7.1 --- a/src/Pure/Isar/locale.ML Fri Oct 28 15:38:41 2011 +0200
7.2 +++ b/src/Pure/Isar/locale.ML Fri Oct 28 17:15:52 2011 +0200
7.3 @@ -425,7 +425,7 @@
7.4 NONE => Morphism.identity
7.5 | SOME export => collect_mixins context (name, morph $> export) $> export);
7.6 val facts' = facts
7.7 - |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin));
7.8 + |> Element.facts_map (Element.transform_ctxt (transfer input $> morph $> mixin));
7.9 in activ_elem (Notes (kind, facts')) input end;
7.10 in
7.11 fold_rev activate notes input
7.12 @@ -562,7 +562,7 @@
7.13 (* Registrations *)
7.14 (fn thy => fold_rev (fn (_, morph) =>
7.15 let
7.16 - val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
7.17 + val args'' = snd args' |> Element.facts_map (Element.transform_ctxt morph) |>
7.18 Attrib.map_facts (Attrib.attribute_i thy)
7.19 in Global_Theory.note_thmss kind args'' #> snd end)
7.20 (registrations_of (Context.Theory thy) loc) thy))
8.1 --- a/src/Pure/Isar/named_target.ML Fri Oct 28 15:38:41 2011 +0200
8.2 +++ b/src/Pure/Isar/named_target.ML Fri Oct 28 17:15:52 2011 +0200
8.3 @@ -118,7 +118,7 @@
8.4 let
8.5 val global_facts' = Attrib.map_facts (K I) global_facts;
8.6 val local_facts' = Element.facts_map
8.7 - (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
8.8 + (Element.transform_ctxt (Local_Theory.target_morphism lthy)) local_facts;
8.9 in
8.10 lthy
8.11 |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
9.1 --- a/src/Pure/raw_simplifier.ML Fri Oct 28 15:38:41 2011 +0200
9.2 +++ b/src/Pure/raw_simplifier.ML Fri Oct 28 17:15:52 2011 +0200
9.3 @@ -33,7 +33,7 @@
9.4 safe_solvers: string list}
9.5 type simproc
9.6 val eq_simproc: simproc * simproc -> bool
9.7 - val morph_simproc: morphism -> simproc -> simproc
9.8 + val transform_simproc: morphism -> simproc -> simproc
9.9 val make_simproc: {name: string, lhss: cterm list,
9.10 proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
9.11 val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
9.12 @@ -625,7 +625,7 @@
9.13
9.14 fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
9.15
9.16 -fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
9.17 +fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
9.18 Simproc
9.19 {name = name,
9.20 lhss = map (Morphism.cterm phi) lhss,
10.1 --- a/src/Pure/simplifier.ML Fri Oct 28 15:38:41 2011 +0200
10.2 +++ b/src/Pure/simplifier.ML Fri Oct 28 17:15:52 2011 +0200
10.3 @@ -195,7 +195,7 @@
10.4 lthy |> Local_Theory.declaration false (fn phi => fn context =>
10.5 let
10.6 val b' = Morphism.binding phi b;
10.7 - val simproc' = morph_simproc phi simproc;
10.8 + val simproc' = transform_simproc phi simproc;
10.9 in
10.10 context
10.11 |> Data.map (fn (ss, tab) =>
10.12 @@ -298,7 +298,7 @@
10.13 (Args.del -- Args.colon >> K (op delsimprocs) ||
10.14 Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
10.15 >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
10.16 - (K (map_ss (fn ss => f (ss, [morph_simproc phi simproc])))));
10.17 + (K (map_ss (fn ss => f (ss, [transform_simproc phi simproc])))));
10.18
10.19 in
10.20
11.1 --- a/src/Tools/interpretation_with_defs.ML Fri Oct 28 15:38:41 2011 +0200
11.2 +++ b/src/Tools/interpretation_with_defs.ML Fri Oct 28 17:15:52 2011 +0200
11.3 @@ -30,7 +30,7 @@
11.4 |-> (fn eqns => fold (fn ((dep, morph), wits) =>
11.5 fn context =>
11.6 Locale.add_registration (dep, morph $> Element.satisfy_morphism
11.7 - (map (Element.morph_witness export') wits))
11.8 + (map (Element.transform_witness export') wits))
11.9 (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
11.10 Option.map (rpair true))
11.11 export context) (deps ~~ witss))