src/Pure/Thy/term_style.ML
changeset 33522 737589bb9bb8
parent 33184 de8cc01e8d9e
child 35625 9c818cab0dd0
equal deleted inserted replaced
33521:a4c54218be62 33522:737589bb9bb8
    17 (* style data *)
    17 (* style data *)
    18 
    18 
    19 fun err_dup_style name =
    19 fun err_dup_style name =
    20   error ("Duplicate declaration of antiquote style: " ^ quote name);
    20   error ("Duplicate declaration of antiquote style: " ^ quote name);
    21 
    21 
    22 structure StyleData = TheoryDataFun
    22 structure StyleData = Theory_Data
    23 (
    23 (
    24   type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
    24   type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
    25   val empty = Symtab.empty;
    25   val empty = Symtab.empty;
    26   val copy = I;
       
    27   val extend = I;
    26   val extend = I;
    28   fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
    27   fun merge data : T = Symtab.merge (eq_snd (op =)) data
    29     handle Symtab.DUP dup => err_dup_style dup;
    28     handle Symtab.DUP dup => err_dup_style dup;
    30 );
    29 );
    31 
    30 
    32 
    31 
    33 (* accessors *)
    32 (* accessors *)