--- a/src/Pure/Isar/specification.ML Sat Mar 17 15:33:08 2012 +0100
+++ b/src/Pure/Isar/specification.ML Sat Mar 17 16:07:03 2012 +0100
@@ -214,7 +214,7 @@
in (b, mx) end);
val name = Thm.def_binding_optional b raw_name;
val ((lhs, (_, raw_th)), lthy2) = lthy
- |> Local_Theory.define (var, ((Binding.suffix_name "_raw" name, []), rhs));
+ |> Local_Theory.define_internal (var, ((Binding.suffix_name "_raw" name, []), rhs));
val th = prove lthy2 raw_th;
val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);