# HG changeset patch
# User wenzelm
# Date 1292624319 -3600
# Node ID ffae1d9bad06e9e4f384afd2cb7bafac892be4a2
# Parent  ff38ea43aadaf7619466eabe3bb62c51ccaf5106# Parent  78c3e472bb35c9942603838d559db662d6c0a4d1
merged;

diff -r ff38ea43aada -r ffae1d9bad06 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Fri Dec 17 23:09:53 2010 +0100
+++ b/src/Pure/General/binding.ML	Fri Dec 17 23:18:39 2010 +0100
@@ -30,6 +30,8 @@
   val prefix: bool -> string -> binding -> binding
   val conceal: binding -> binding
   val str_of: binding -> string
+  val bad: binding -> string
+  val check: binding -> unit
 end;
 
 structure Binding: BINDING =
@@ -127,6 +129,16 @@
   qualified_name_of binding
   |> Markup.markup (Position.markup (pos_of binding) (Markup.binding (name_of binding)));
 
+
+(* check *)
+
+fun bad binding =
+  "Bad name binding: " ^ quote (str_of binding) ^ Position.str_of (pos_of binding);
+
+fun check binding =
+  if Symbol.is_ident (Symbol.explode (name_of binding)) then ()
+  else legacy_feature (bad binding);
+
 end;
 end;
 
diff -r ff38ea43aada -r ffae1d9bad06 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Dec 17 23:09:53 2010 +0100
+++ b/src/Pure/General/name_space.ML	Fri Dec 17 23:18:39 2010 +0100
@@ -266,11 +266,11 @@
 
 (* full name *)
 
+fun err_bad binding = error (Binding.bad binding);
+
 fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
   | transform_binding _ = I;
 
-fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
-
 fun name_spec (naming as Naming {path, ...}) raw_binding =
   let
     val binding = transform_binding naming raw_binding;
diff -r ff38ea43aada -r ffae1d9bad06 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Fri Dec 17 23:09:53 2010 +0100
+++ b/src/Pure/consts.ML	Fri Dec 17 23:18:39 2010 +0100
@@ -235,6 +235,7 @@
   map_consts (fn (decls, constraints, rev_abbrevs) =>
     let
       val decl = {T = declT, typargs = typargs_of declT};
+      val _ = Binding.check b;
       val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
     in (decls', constraints, rev_abbrevs) end);
 
@@ -287,6 +288,7 @@
       let
         val decl = {T = T, typargs = typargs_of T};
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
+        val _ = Binding.check b;
         val (_, decls') = decls
           |> Name_Space.define true naming (b, (decl, SOME abbr));
         val rev_abbrevs' = rev_abbrevs
diff -r ff38ea43aada -r ffae1d9bad06 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Dec 17 23:09:53 2010 +0100
+++ b/src/Pure/simplifier.ML	Fri Dec 17 23:18:39 2010 +0100
@@ -112,7 +112,9 @@
 );
 
 val get_ss = Simpset.get;
-fun map_ss f context = Simpset.map (with_context (Context.proof_of context) f) context;
+
+fun map_ss f context =
+  Simpset.map (Raw_Simplifier.with_context (Context.proof_of context) f) context;
 
 
 (* attributes *)
@@ -231,7 +233,7 @@
       (rev (if safe then solvers else unsafe_solvers)));
 
     fun simp_loop_tac i =
-      asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
+      Raw_Simplifier.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   in simp_loop_tac end;
 
diff -r ff38ea43aada -r ffae1d9bad06 src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Dec 17 23:09:53 2010 +0100
+++ b/src/Pure/type.ML	Fri Dec 17 23:18:39 2010 +0100
@@ -418,10 +418,10 @@
 
 fun typ_match tsig =
   let
-    fun match (T0 as TVar (v, S), T) subs = 
+    fun match (T0 as TVar (v, S), T) subs =
           (case lookup subs (v, S) of
             NONE =>
-              if of_sort tsig (T, S) 
+              if of_sort tsig (T, S)
               then if T0 = T then subs (*types already identical; don't create cycle!*)
                    else Vartab.update_new (v, (S, T)) subs
               else raise TYPE_MATCH
@@ -582,6 +582,7 @@
     let
       val cs' = map (cert_class tsig) cs
         handle TYPE (msg, _, _) => error msg;
+      val _ = Binding.check c;
       val (c', space') = space |> Name_Space.declare true naming c;
       val classes' = classes |> Sorts.add_class pp (c', cs');
     in ((space', classes'), default, types) end);
@@ -627,7 +628,7 @@
 local
 
 fun new_decl naming (c, decl) types =
-  #2 (Name_Space.define true naming (c, decl) types);
+  (Binding.check c; #2 (Name_Space.define true naming (c, decl) types));
 
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let