diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Thy/term_style.ML --- a/src/Pure/Thy/term_style.ML Sun May 06 21:50:17 2007 +0200 +++ b/src/Pure/Thy/term_style.ML Mon May 07 00:49:59 2007 +0200 @@ -22,19 +22,17 @@ error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names); structure StyleData = TheoryDataFun -(struct - val name = "Isar/antiquote_style"; +( type T = ((Proof.context -> term -> term) * stamp) Symtab.table; val empty = Symtab.empty; val copy = I; val extend = I; fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs handle Symtab.DUPS dups => err_dup_styles dups; - fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab)); -end); +); -val _ = Context.add_setup StyleData.init; -val print_styles = StyleData.print; +fun print_styles thy = + Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys (StyleData.get thy))); (* accessors *)