Nominal/nominal_function.ML
changeset 3135 92b9b8d2888d
parent 3045 d0ad264f8c4f
child 3165 31c64dd4c95a
--- 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