notation: improved ProofContext.read_const does the job;
authorwenzelm
Sat Nov 10 14:31:21 2007 +0100 (2007-11-10)
changeset 2537126d349416c4f
parent 25370 8b1aa4357320
child 25372 a718f1ccaf1a
notation: improved ProofContext.read_const does the job;
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Sat Nov 10 14:31:20 2007 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Sat Nov 10 14:31:21 2007 +0100
     1.3 @@ -204,16 +204,7 @@
     1.4  (* notation *)
     1.5  
     1.6  fun gen_notation prep_const add mode args lthy =
     1.7 -  let
     1.8 -    val ctxt = ProofContext.set_mode ProofContext.mode_abbrev lthy;
     1.9 -    fun prep_arg (s, mx) =
    1.10 -      let
    1.11 -        val t = Syntax.check_term ctxt
    1.12 -          (case prep_const ctxt s of Const (c, _) => Const (c, dummyT) | a => a);
    1.13 -        val [t'] = Syntax.uncheck_terms ctxt [t];
    1.14 -        val u = if Term.is_Const t' orelse Term.is_Free t' then t' else t;
    1.15 -      in (u, mx) end;
    1.16 -  in lthy |> LocalTheory.notation add mode (map prep_arg args) end;
    1.17 +  lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args);
    1.18  
    1.19  val notation = gen_notation (K I);
    1.20  val notation_cmd = gen_notation ProofContext.read_const;