notation: improved ProofContext.read_const does the job;

--- a/src/Pure/Isar/specification.ML	Sat Nov 10 14:31:20 2007 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Nov 10 14:31:21 2007 +0100
@@ -204,16 +204,7 @@
 (* notation *)
 
 fun gen_notation prep_const add mode args lthy =
-  let
-    val ctxt = ProofContext.set_mode ProofContext.mode_abbrev lthy;
-    fun prep_arg (s, mx) =
-      let
-        val t = Syntax.check_term ctxt
-          (case prep_const ctxt s of Const (c, _) => Const (c, dummyT) | a => a);
-        val [t'] = Syntax.uncheck_terms ctxt [t];
-        val u = if Term.is_Const t' orelse Term.is_Free t' then t' else t;
-      in (u, mx) end;
-  in lthy |> LocalTheory.notation add mode (map prep_arg args) end;
+  lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args);
 
 val notation = gen_notation (K I);
 val notation_cmd = gen_notation ProofContext.read_const;