src/Pure/Isar/local_theory.ML
changeset 38381 7d1e2a6831ec
parent 38308 0e4649095739
child 38756 d07959fabde6
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed Aug 11 17:16:02 2010 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Aug 11 17:19:27 2010 +0200
     1.3 @@ -50,7 +50,6 @@
     1.4    val const_alias: binding -> string -> local_theory -> local_theory
     1.5    val init: serial option -> string -> operations -> Proof.context -> local_theory
     1.6    val restore: local_theory -> local_theory
     1.7 -  val reinit: local_theory -> local_theory
     1.8    val exit: local_theory -> Proof.context
     1.9    val exit_global: local_theory -> theory
    1.10    val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
    1.11 @@ -75,7 +74,6 @@
    1.12    declaration: bool -> declaration -> local_theory -> local_theory,
    1.13    syntax_declaration: bool -> declaration -> local_theory -> local_theory,
    1.14    pretty: local_theory -> Pretty.T list,
    1.15 -  reinit: local_theory -> local_theory,
    1.16    exit: local_theory -> Proof.context};
    1.17  
    1.18  datatype lthy = LThy of
    1.19 @@ -260,8 +258,6 @@
    1.20    let val {naming, theory_prefix, operations, target} = get_lthy lthy
    1.21    in init (Name_Space.get_group naming) theory_prefix operations target end;
    1.22  
    1.23 -val reinit = checkpoint o operation #reinit;
    1.24 -
    1.25  
    1.26  (* exit *)
    1.27