src/Pure/Tools/plugin.ML
changeset 59058 a78612c67ec0
parent 58668 1891f17c6124
child 59145 0e304b1568a5
     1.1 --- a/src/Pure/Tools/plugin.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/Pure/Tools/plugin.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -112,8 +112,8 @@
     1.4  type data = {filter: Plugin_Name.filter, naming: Name_Space.naming, value: T, id: serial};
     1.5  type interp = {name: string, apply: T -> local_theory -> local_theory, id: serial};
     1.6  
     1.7 -val eq_data: data * data -> bool = op = o pairself #id;
     1.8 -val eq_interp: interp * interp -> bool = op = o pairself #id;
     1.9 +val eq_data: data * data -> bool = op = o apply2 #id;
    1.10 +val eq_interp: interp * interp -> bool = op = o apply2 #id;
    1.11  
    1.12  fun mk_data filter naming x : data = {filter = filter, naming = naming, value = x, id = serial ()};
    1.13  fun mk_interp name f : interp = {name = name, apply = f, id = serial ()};