more operations;
authorwenzelm
Mon Jan 08 15:50:11 2018 +0100 (17 months ago ago)
changeset 67376d5007d93bcc6
parent 67375 c0c36348a4fb
child 67377 143665524d8e
more operations;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Jan 08 14:59:50 2018 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jan 08 15:50:11 2018 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    exception UNDEF
     1.6    type state
     1.7 +  val generic_theory_toplevel: generic_theory -> state
     1.8    val theory_toplevel: theory -> state
     1.9    val toplevel: state
    1.10    val is_toplevel: state -> bool
    1.11 @@ -120,7 +121,8 @@
    1.12  
    1.13  datatype state = State of node option * node option;  (*current, previous*)
    1.14  
    1.15 -fun theory_toplevel thy = State (SOME (Theory (Context.Theory thy, NONE)), NONE);
    1.16 +fun generic_theory_toplevel gthy = State (SOME (Theory (gthy, NONE)), NONE);
    1.17 +val theory_toplevel = generic_theory_toplevel o Context.Theory;
    1.18  
    1.19  val toplevel = State (NONE, NONE);
    1.20