src/Pure/Isar/named_target.ML
changeset 45488 6d71d9e52369
parent 45390 e29521ef9059
child 45581 ac32737ff69e
     1.1 --- a/src/Pure/Isar/named_target.ML	Mon Nov 14 16:24:50 2011 +0100
     1.2 +++ b/src/Pure/Isar/named_target.ML	Mon Nov 14 16:52:19 2011 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4    val init: (local_theory -> local_theory) -> string -> theory -> local_theory
     1.5    val theory_init: theory -> local_theory
     1.6    val reinit: local_theory -> local_theory -> local_theory
     1.7 -  val context_cmd: xstring -> theory -> local_theory
     1.8 +  val context_cmd: xstring * Position.T -> theory -> local_theory
     1.9    val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
    1.10  end;
    1.11  
    1.12 @@ -209,7 +209,7 @@
    1.13        init before_exit target o Local_Theory.exit_global
    1.14    | NONE => error "Not in a named target");
    1.15  
    1.16 -fun context_cmd "-" thy = init I "" thy
    1.17 -  | context_cmd target thy = init I (Locale.intern thy target) thy;
    1.18 +fun context_cmd ("-", _) thy = init I "" thy
    1.19 +  | context_cmd target thy = init I (Locale.check thy target) thy;
    1.20  
    1.21  end;