--- a/QuotTest.thy	Tue Nov 10 17:43:05 2009 +0100
+++ b/QuotTest.thy	Wed Nov 11 10:22:47 2009 +0100
@@ -98,9 +98,7 @@
 (* A test whether get_fun works properly
 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
 local_setup {*
-  fn lthy => (Toplevel.program (fn () =>
-    make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
-  )) |> snd
+    make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |> snd
 *}
 *)