# HG changeset patch
# User wenzelm
# Date 1436349043 -7200
# Node ID 0568c7a2b5dbb343d819bf64ab9879e20c210bda
# Parent  53a71c9203b21c107da2561aff93fa216139f026
tuned according to a81dc82ecba3;

diff -r 53a71c9203b2 -r 0568c7a2b5db src/Pure/Isar/outer_syntax.ML
--- 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