--- a/src/Pure/Isar/specification.ML Mon Apr 25 16:09:26 2016 +0200
+++ b/src/Pure/Isar/specification.ML Mon Apr 25 16:54:48 2016 +0200
@@ -249,7 +249,7 @@
error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
Position.here (Binding.pos_of b));
in (b, mx) end);
- val name = Binding.reset_pos (Thm.def_binding_optional b raw_name);
+ val name = Thm.def_binding_optional b raw_name;
val ((lhs, (_, raw_th)), lthy2) = lthy
|> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));