# HG changeset patch
# User wenzelm
# Date 1193429443 -7200
# Node ID aec1cbdbca7160012a1c8e7867550a41555de0ab
# Parent  5b5659801257a17e93f233f8bf5c3900d404790e
notation: associate syntax to checked-unchecked term;

diff -r 5b5659801257 -r aec1cbdbca71 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Oct 26 22:10:42 2007 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Oct 26 22:10:43 2007 +0200
@@ -204,7 +204,16 @@
 (* notation *)
 
 fun gen_notation prep_const add mode args lthy =
-  lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args);
+  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;
 
 val notation = gen_notation (K I);
 val notation_cmd = gen_notation ProofContext.read_const;