--- a/src/HOL/Tools/Function/fun.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Function/fun.ML Mon May 17 23:54:15 2010 +0200
@@ -159,13 +159,10 @@
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
+ Outer_Syntax.local_theory "fun" "define general recursive functions (short version)"
+ Keyword.thy_decl
(function_parser fun_config
- >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config));
+ >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
end
-
-end