--- a/src/Pure/Isar/outer_syntax.ML Wed Jul 08 00:04:15 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Jul 08 11:50:43 2015 +0200
@@ -45,7 +45,7 @@
datatype command_parser =
Parser of (Toplevel.transition -> Toplevel.transition) parser |
- Limited_Parser of
+ Restricted_Parser of
(bool * Position.T) option -> (Toplevel.transition -> Toplevel.transition) parser;
datatype command = Command of
@@ -147,8 +147,8 @@
fun local_theory_command trans command_keyword comment parse =
raw_command command_keyword comment
- (Limited_Parser (fn limited =>
- Parse.opt_target -- parse >> (fn (target, f) => trans limited target f)));
+ (Restricted_Parser (fn restricted =>
+ Parse.opt_target -- parse >> (fn (target, f) => trans restricted target f)));
val local_theory' = local_theory_command Toplevel.local_theory';
val local_theory = local_theory_command Toplevel.local_theory;
@@ -178,9 +178,9 @@
(case lookup_commands thy name of
SOME (Command {command_parser = Parser parse, ...}) =>
Parse.!!! (command_tags |-- parse) >> (fn f => f tr0)
- | SOME (Command {command_parser = Limited_Parser parse, ...}) =>
- before_command :|-- (fn limited =>
- Parse.!!! (command_tags |-- parse limited)) >> (fn f => f tr0)
+ | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
+ before_command :|-- (fn restricted =>
+ Parse.!!! (command_tags |-- parse restricted)) >> (fn f => f tr0)
| NONE =>
Scan.fail_with (fn _ => fn _ =>
let