--- a/src/Pure/Isar/isar_syn.ML Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sun Apr 17 19:54:04 2011 +0200
@@ -129,7 +129,7 @@
val _ =
Outer_Syntax.command "nonterminal"
"declare syntactic type constructors (grammar nonterminal symbols)" Keyword.thy_decl
- (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
+ (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
val _ =
Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl