rename one of the two 'rel_eq_thms' to 'rel_code_thms'
authordesharna
Mon, 06 Oct 2014 13:40:02 +0200
changeset 58582 a408c72a849c
parent 58581 e2e2d775869c
child 58583 1dd83cbba636
rename one of the two 'rel_eq_thms' to 'rel_code_thms'
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:39:12 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:40:02 2014 +0200
@@ -649,7 +649,7 @@
       val (rel_distinct_thms, _) =
         join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
 
-      val rel_eq_thms =
+      val rel_code_thms =
         map (fn thm => thm RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @
         map2 (fn thm => fn 0 => thm RS @{thm eq_True[THEN iffD2]} | _ => thm) rel_inject_thms ms;
 
@@ -986,7 +986,7 @@
       val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
 
       val anonymous_notes =
-        [(rel_eq_thms, code_attrs @ nitpicksimp_attrs)]
+        [(rel_code_thms, code_attrs @ nitpicksimp_attrs)]
         |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
       val notes =
@@ -1011,7 +1011,7 @@
         lthy
         |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms)
         |> fp = Least_FP
-          ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms)
+          ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_code_thms)
         |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set0_thms)
         |> Local_Theory.notes (anonymous_notes @ notes);