| changeset 45294 | 3c5d3d286055 |
| parent 45008 | 8b74cfea913a |
| child 45403 | 7a0b8debef77 |
--- a/src/HOL/Tools/Function/partial_function.ML Fri Oct 28 23:16:50 2011 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Fri Oct 28 23:41:16 2011 +0200 @@ -53,7 +53,7 @@ structure Mono_Rules = Named_Thms ( - val name = "partial_function_mono"; + val name = @{binding partial_function_mono}; val description = "monotonicity rules for partial function definitions"; );