diff -r 7ee65dbffa31 -r b61d52de66f0 src/HOL/Mutabelle/MutabelleExtra.thy
--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Oct 25 21:06:56 2010 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Oct 25 21:23:09 2010 +0200
@@ -19,10 +19,11 @@
      "mutabelle_extra.ML"
 begin
 
-ML {* val old_tr = !Output.tracing_fn *}
-ML {* val old_wr = !Output.writeln_fn *}
-ML {* val old_ur = !Output.urgent_message_fn *}
-ML {* val old_wa = !Output.warning_fn *}
+(* FIXME !?!?! *)
+ML {* val old_tr = !Output.Private_Hooks.tracing_fn *}
+ML {* val old_wr = !Output.Private_Hooks.writeln_fn *}
+ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *}
+ML {* val old_wa = !Output.Private_Hooks.warning_fn *}
 
 quickcheck_params [size = 5, iterations = 1000]
 (*
@@ -48,9 +49,10 @@
 *)
  *}
 
-ML {* Output.tracing_fn := old_tr *}
-ML {* Output.writeln_fn := old_wr *}
-ML {* Output.urgent_message_fn := old_ur *}
-ML {* Output.warning_fn := old_wa *}
+(* FIXME !?!?! *)
+ML {* Output.Private_Hooks.tracing_fn := old_tr *}
+ML {* Output.Private_Hooks.writeln_fn := old_wr *}
+ML {* Output.Private_Hooks.urgent_message_fn := old_ur *}
+ML {* Output.Private_Hooks.warning_fn := old_wa *}
 
 end