src/Pure/Isar/local_theory.ML
changeset 36004 5d79ca55a52b
parent 35798 fd1bb29f8170
child 36451 ddc965e172c4
     1.1 --- a/src/Pure/Isar/local_theory.ML	Sun Mar 28 17:43:09 2010 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sun Mar 28 19:20:52 2010 +0200
     1.3 @@ -20,7 +20,6 @@
     1.4    val target_of: local_theory -> Proof.context
     1.5    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     1.6    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     1.7 -  val checkpoint: local_theory -> local_theory
     1.8    val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     1.9    val theory: (theory -> theory) -> local_theory -> local_theory
    1.10    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
    1.11 @@ -149,7 +148,8 @@
    1.12      thy
    1.13      |> Sign.map_naming (K (naming_of lthy))
    1.14      |> f
    1.15 -    ||> Sign.restore_naming thy);
    1.16 +    ||> Sign.restore_naming thy
    1.17 +    ||> Theory.checkpoint);
    1.18  
    1.19  fun theory f = #2 o theory_result (f #> pair ());
    1.20