# HG changeset patch
# User wenzelm
# Date 1427218589 -3600
# Node ID 0b21e85fd9bab62ddaa003657ac0535c023146a0
# Parent  45c89526208f0c6cb4ed3cdb162a7d30ab199da1
clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;

diff -r 45c89526208f -r 0b21e85fd9ba src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 24 16:17:07 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 24 18:36:29 2015 +0100
@@ -608,10 +608,13 @@
 fun is_free_in frees (Free (v, _)) = member (op =) frees v
   | is_free_in _ _ = false;
 
+fun is_catch_all_prem (Free (v, _)) = v = Name.uu_
+  | is_catch_all_prem _ = false;
+
 fun add_extra_frees ctxt frees names =
   fold_aterms (fn x as Free (v, _) =>
     (not (member (op =) frees x) andalso not (member (op =) names v) andalso
-     not (Variable.is_fixed ctxt v) andalso v <> Name.uu_)
+     not (Variable.is_fixed ctxt v) andalso not (is_catch_all_prem x))
     ? cons x | _ => I);
 
 fun check_extra_frees ctxt frees names t =
@@ -678,9 +681,6 @@
     val ctr_no = if not_disc then 1 - ctr_no' else ctr_no';
     val {ctr, disc, ...} = nth basic_ctr_specs ctr_no;
 
-    fun is_catch_all_prem (Free (s, _)) = s = Name.uu_
-      | is_catch_all_prem _ = false;
-
     val catch_all =
       (case prems0 of
         [prem] => is_catch_all_prem prem