--- 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;