src/Pure/Isar/toplevel.ML
changeset 49010 72808e956879
parent 48993 44428ea53dc1
child 49011 9c68e43502ce
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Aug 30 15:26:37 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Aug 30 16:39:50 2012 +0200
     1.3 @@ -426,11 +426,11 @@
     1.4  
     1.5  val global_theory_group =
     1.6    Sign.new_group #>
     1.7 -  Global_Theory.begin_recent_proofs #> Theory.checkpoint;
     1.8 +  Thm.begin_recent_proofs #> Theory.checkpoint;
     1.9  
    1.10  val local_theory_group =
    1.11    Local_Theory.new_group #>
    1.12 -  Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
    1.13 +  Local_Theory.raw_theory (Thm.begin_recent_proofs #> Theory.checkpoint);
    1.14  
    1.15  fun generic_theory f = transaction (fn _ =>
    1.16    (fn Theory (gthy, _) => Theory (f gthy, NONE)