# HG changeset patch
# User wenzelm
# Date 1206814453 -3600
# Node ID c93ff30790fe27791498fbb8083ffe5a30d12691
# Parent  87d27e426f14282273eb9c3852ca86985deb8162
added generic_theory transaction;

diff -r 87d27e426f14 -r c93ff30790fe src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Mar 29 19:14:12 2008 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Mar 29 19:14:13 2008 +0100
@@ -68,6 +68,7 @@
   val keep': (bool -> state -> unit) -> transition -> transition
   val imperative: (unit -> unit) -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
+  val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
   val end_local_theory: transition -> transition
@@ -524,6 +525,10 @@
 
 (* theory transitions *)
 
+fun generic_theory f = app_current (fn _ =>
+  (fn Theory (gthy, _) => Theory (f gthy, NONE)
+    | _ => raise UNDEF));
+
 fun theory' f = app_current (fn int =>
   (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (f int thy), NONE)
     | _ => raise UNDEF));