# HG changeset patch
# User wenzelm
# Date 1194701481 -3600
# Node ID 26d349416c4f565b46c8dbd35d3b4f27b9ccc700
# Parent  8b1aa43573206f6d5b5f19bb0f4a87bbe1acf97d
notation: improved ProofContext.read_const does the job;

diff -r 8b1aa4357320 -r 26d349416c4f src/Pure/Isar/specification.ML
--- 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;