| changeset 51788 | 5fe72280a49f |
| parent 51787 | 1267c28c7bdd |
| child 51790 | 22517d04d20b |
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Apr 26 11:04:45 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Apr 26 11:04:46 2013 +0200 @@ -31,7 +31,7 @@ open BNF_FP open BNF_FP_Def_Sugar_Tactics -val EqN = "Eq"; +val EqN = "Eq_"; (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) fun quasi_unambiguous_case_names names =