# HG changeset patch
# User wenzelm
# Date 1395047483 -3600
# Node ID 9b0dc5c704c91dc8f0fec437c426dbdb9e3d9e32
# Parent  088b64497a6149720fcd8e64546fe3a86c9ac20b
reject internal names, notably from Term.free_dummy_patterns;

diff -r 088b64497a61 -r 9b0dc5c704c9 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Mar 17 10:01:58 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Mon Mar 17 10:11:23 2014 +0100
@@ -200,6 +200,7 @@
   let
     val (vars, [((raw_name, atts), prop)]) = fst (prep (the_list raw_var) [raw_spec] lthy);
     val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
+    val _ = Name.reject_internal (x, []);
     val var as (b, _) =
       (case vars of
         [] => (Binding.name x, NoSyn)
@@ -240,6 +241,7 @@
       prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
         (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
     val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
+    val _ = Name.reject_internal (x, []);
     val var =
       (case vars of
         [] => (Binding.name x, NoSyn)