src/Pure/Isar/toplevel.ML
changeset 45488 6d71d9e52369
parent 44304 7ee000ce5390
child 45666 d83797ef0d2d
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Nov 14 16:24:50 2011 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Nov 14 16:52:19 2011 +0100
     1.3 @@ -58,14 +58,16 @@
     1.4    val theory': (bool -> theory -> theory) -> transition -> transition
     1.5    val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
     1.6    val end_local_theory: transition -> transition
     1.7 -  val local_theory': xstring option -> (bool -> local_theory -> local_theory) ->
     1.8 +  val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
     1.9 +    transition -> transition
    1.10 +  val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
    1.11      transition -> transition
    1.12 -  val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
    1.13 -  val present_local_theory: xstring option -> (state -> unit) -> transition -> transition
    1.14 -  val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
    1.15 +  val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
    1.16      transition -> transition
    1.17 -  val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
    1.18 -    transition -> transition
    1.19 +  val local_theory_to_proof': (xstring * Position.T) option ->
    1.20 +    (bool -> local_theory -> Proof.state) -> transition -> transition
    1.21 +  val local_theory_to_proof: (xstring * Position.T) option ->
    1.22 +    (local_theory -> Proof.state) -> transition -> transition
    1.23    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
    1.24    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
    1.25    val forget_proof: transition -> transition
    1.26 @@ -105,7 +107,7 @@
    1.27  val loc_init = Named_Target.context_cmd;
    1.28  val loc_exit = Local_Theory.exit_global;
    1.29  
    1.30 -fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
    1.31 +fun loc_begin loc (Context.Theory thy) = loc_init (the_default ("-", Position.none) loc) thy
    1.32    | loc_begin NONE (Context.Proof lthy) = lthy
    1.33    | loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy;
    1.34