# HG changeset patch
# User blanchet
# Date 1473700957 -7200
# Node ID 0db1481c1ec1ed2982fe6abb5b45233e11c15012
# Parent  40f34614bd06b83bc535e4628bb2a5a1412c41c1
moved ML function

diff -r 40f34614bd06 -r 0db1481c1ec1 src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML	Mon Sep 12 17:32:09 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML	Mon Sep 12 19:22:37 2016 +0200
@@ -111,8 +111,6 @@
     rho_def dtor_algrho corecUU_unique eq_corecUU all_sig_maps ssig_map_thms
     all_algLam_alg_pointfuls all_algrho_eqs eval_simps =
   let
-    fun mk_abs_def thm = Drule.abs_def (thm RS eq_reflection);
-
     val nullary_disc_defs' = nullary_disc_defs
       |> map (fn thm => thm RS sym)
       |> maps (fn thm => [thm, thm RS @{thm subst[OF eq_commute, of "%e. e = z" for z]}]);
diff -r 40f34614bd06 -r 0db1481c1ec1 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Sep 12 17:32:09 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Sep 12 19:22:37 2016 +0200
@@ -46,6 +46,7 @@
 
   val mk_disjIN: int -> int -> thm
 
+  val mk_abs_def: thm -> thm
   val mk_unabs_def: int -> thm -> thm
 
   val mk_IfN: typ -> term list -> term list -> term
@@ -193,6 +194,7 @@
   | mk_disjIN 2 2 = disjI2
   | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
 
+fun mk_abs_def thm = Drule.abs_def (thm RS eq_reflection handle THM _ => thm);
 fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
 
 fun mk_IfN _ _ [t] = t