--- 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 *)