--- a/src/HOL/Tools/record.ML Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/record.ML Fri Nov 29 20:57:04 2019 +0100
@@ -1813,9 +1813,8 @@
| lhs_of_equation (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _)) = t;
fun add_spec_rule rule =
- let val head = head_of (lhs_of_equation (Thm.prop_of rule)) in
- Spec_Rules.add_global Spec_Rules.equational ([head], [rule])
- end;
+ let val head = head_of (lhs_of_equation (Thm.prop_of rule))
+ in Spec_Rules.add_global "" Spec_Rules.equational [head] [rule] end;
(* definition *)