diff -r 301b74fcd614 -r 92b9b8d2888d Nominal/nominal_function.ML --- 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