| changeset 36954 | ef698bd61057 |
| parent 36692 | 54b64d4ad524 |
| child 36960 | 01594f816e3a |
--- a/src/HOL/Tools/Function/function_common.ML Sat May 15 23:40:00 2010 +0200 +++ b/src/HOL/Tools/Function/function_common.ML Sun May 16 00:02:11 2010 +0200 @@ -355,7 +355,7 @@ >> (fn opts => fold apply_opt opts default) in fun function_parser default_cfg = - config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs + config_parser default_cfg -- P.fixes -- Parse_Spec.where_alt_specs end