--- a/src/HOL/Tools/inductive_set.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/inductive_set.ML Wed Dec 16 16:31:36 2015 +0100
@@ -349,7 +349,7 @@
Rule_Cases.save thm
end;
-val to_pred_att = Thm.rule_attribute o to_pred;
+val to_pred_att = Thm.rule_attribute [] o to_pred;
(**** convert theorem in predicate notation to set notation ****)
@@ -385,7 +385,7 @@
Rule_Cases.save thm
end;
-val to_set_att = Thm.rule_attribute o to_set;
+val to_set_att = Thm.rule_attribute [] o to_set;
(**** definition of inductive sets ****)