# HG changeset patch
# User blanchet
# Date 1402422660 -7200
# Node ID c7b06cdf108a9a3a21ad78240118175ea3aacc13
# Parent  7c36ce8e45f68462bacb880ba9b0494151a3b70a
tuning

diff -r 7c36ce8e45f6 -r c7b06cdf108a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 10 19:15:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 10 19:51:00 2014 +0200
@@ -181,8 +181,6 @@
 val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
 val simp_attrs = @{attributes [simp]};
 
-fun is_triv_eq t = op aconv (HOLogic.dest_eq t) handle TERM _ => false;
-
 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
 
 fun flat_corec_predss_getterss qss gss = maps (op @) (qss ~~ gss);
@@ -1197,7 +1195,7 @@
                       val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discsA;
 
                       fun mk_goal (discA_t, discB) =
-                        if head_of discA_t aconv HOLogic.Not orelse is_triv_eq discA_t then
+                        if head_of discA_t aconv HOLogic.Not orelse is_refl_bool discA_t then
                           NONE
                         else
                           SOME (mk_Trueprop_eq
@@ -1232,7 +1230,7 @@
                             | _ => map_rhs $ (selA $ ta));
                           val concl = mk_Trueprop_eq (lhs, rhs);
                         in
-                          if is_triv_eq prem then concl
+                          if is_refl_bool prem then concl
                           else Logic.mk_implies (HOLogic.mk_Trueprop prem, concl)
                         end;
                       val goals = map mk_goal disc_sel_pairs;
@@ -1292,7 +1290,7 @@
                               travese_nested_types (selA $ ta) names_lthy;
                         in
                           if exists_subtype_in [A] sel_rangeT then
-                            if is_triv_eq prem then
+                            if is_refl_bool prem then
                               (concls, ctxt')
                             else
                               (map (Logic.mk_implies o pair (HOLogic.mk_Trueprop prem)) concls,
@@ -1542,8 +1540,8 @@
   define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term x;
 
 val parse_ctr_arg =
-  @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
-  (Parse.typ >> pair Binding.empty);
+  @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"}
+  || Parse.typ >> pair Binding.empty;
 
 val parse_ctr_specs =
   Parse.enum1 "|" (parse_ctr_spec Parse.binding parse_ctr_arg -- Parse.opt_mixfix);
diff -r 7c36ce8e45f6 -r c7b06cdf108a src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Tue Jun 10 19:15:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Tue Jun 10 19:51:00 2014 +0200
@@ -136,6 +136,7 @@
   val mk_sym: thm -> thm
   val mk_trans: thm -> thm -> thm
 
+  val is_refl_bool: term -> bool
   val is_refl: thm -> bool
   val is_concl_refl: thm -> bool
   val no_refl: thm list -> thm list
@@ -327,7 +328,6 @@
   end;
 
 
-
 (* Term construction *)
 
 (** Fresh variables **)
@@ -577,6 +577,10 @@
     | mk_UnIN n m = mk_UnIN' (n - m)
 end;
 
+fun is_refl_bool t =
+  op aconv (HOLogic.dest_eq t)
+  handle TERM _ => false;
+
 fun is_refl_prop t =
   op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop t))
   handle TERM _ => false;