# HG changeset patch # User wenzelm # Date 1575300503 -3600 # Node ID 2dee5cd42fde61b9afe50ded50de5145d4c00c7d # Parent e64c249d3d98b8db8e23684fde95f75a7412e37c clarified name: avoid clashes; diff -r e64c249d3d98 -r 2dee5cd42fde src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Mon Dec 02 16:15:27 2019 +0100 +++ b/src/Pure/Isar/specification.ML Mon Dec 02 16:28:23 2019 +0100 @@ -269,7 +269,7 @@ |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs)); val th = prove lthy2 raw_th; - val lthy3 = lthy2 |> Spec_Rules.add b Spec_Rules.equational [lhs] [th]; + val lthy3 = lthy2 |> Spec_Rules.add name Spec_Rules.equational [lhs] [th]; val ([(def_name, [th'])], lthy4) = lthy3 |> Local_Theory.notes [((name, atts), [([th], [])])];