src/Pure/Thy/term_style.ML
changeset 33522 737589bb9bb8
parent 33184 de8cc01e8d9e
child 35625 9c818cab0dd0
--- a/src/Pure/Thy/term_style.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Thy/term_style.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -19,13 +19,12 @@
 fun err_dup_style name =
   error ("Duplicate declaration of antiquote style: " ^ quote name);
 
-structure StyleData = TheoryDataFun
+structure StyleData = Theory_Data
 (
   type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
+  fun merge data : T = Symtab.merge (eq_snd (op =)) data
     handle Symtab.DUP dup => err_dup_style dup;
 );