src/Pure/Thy/term_style.ML
changeset 22846 fb79144af9a3
parent 22107 926afa3361e1
child 23577 c5b93c69afd3
--- 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 *)