--- a/Nominal/nominal_function.ML Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/nominal_function.ML Tue Mar 20 11:26:10 2012 +0000
@@ -275,10 +275,10 @@
(* nominal *)
val _ =
- Outer_Syntax.local_theory_to_proof' "nominal_primrec" "define general recursive nominal functions"
- Keyword.thy_goal
- (nominal_function_parser nominal_default_config
- >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
+ Outer_Syntax.local_theory_to_proof' ("nominal_primrec", Keyword.thy_goal)
+ "define general recursive nominal functions"
+ (nominal_function_parser nominal_default_config
+ >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
end