added generic_theory transaction;
authorwenzelm
Sat Mar 29 19:14:13 2008 +0100 (2008-03-29 ago)
changeset 26491c93ff30790fe
parent 26490 87d27e426f14
child 26492 6e87cc839632
added generic_theory transaction;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Mar 29 19:14:12 2008 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Mar 29 19:14:13 2008 +0100
     1.3 @@ -68,6 +68,7 @@
     1.4    val keep': (bool -> state -> unit) -> transition -> transition
     1.5    val imperative: (unit -> unit) -> transition -> transition
     1.6    val theory: (theory -> theory) -> transition -> transition
     1.7 +  val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
     1.8    val theory': (bool -> theory -> theory) -> transition -> transition
     1.9    val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
    1.10    val end_local_theory: transition -> transition
    1.11 @@ -524,6 +525,10 @@
    1.12  
    1.13  (* theory transitions *)
    1.14  
    1.15 +fun generic_theory f = app_current (fn _ =>
    1.16 +  (fn Theory (gthy, _) => Theory (f gthy, NONE)
    1.17 +    | _ => raise UNDEF));
    1.18 +
    1.19  fun theory' f = app_current (fn int =>
    1.20    (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (f int thy), NONE)
    1.21      | _ => raise UNDEF));