src/Pure/sign.ML
changeset 35255 2cb27605301f
parent 35200 aaddb2b526d6
child 35262 9ea4445d2ccf
     1.1 --- a/src/Pure/sign.ML	Sun Feb 21 21:04:17 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Sun Feb 21 21:08:25 2010 +0100
     1.3 @@ -41,7 +41,6 @@
     1.4    val declared_tyname: theory -> string -> bool
     1.5    val declared_const: theory -> string -> bool
     1.6    val const_monomorphic: theory -> string -> bool
     1.7 -  val const_syntax_name: theory -> string -> string
     1.8    val const_typargs: theory -> string * typ -> typ list
     1.9    val const_instance: theory -> string * typ list -> typ
    1.10    val mk_const: theory -> string * typ list -> term
    1.11 @@ -59,7 +58,7 @@
    1.12    val intern_typ: theory -> typ -> typ
    1.13    val extern_typ: theory -> typ -> typ
    1.14    val intern_term: theory -> term -> term
    1.15 -  val extern_term: (string -> xstring) -> theory -> term -> term
    1.16 +  val extern_term: theory -> term -> term
    1.17    val intern_tycons: theory -> typ -> typ
    1.18    val arity_number: theory -> string -> int
    1.19    val arity_sorts: theory -> string -> sort -> sort list
    1.20 @@ -226,7 +225,6 @@
    1.21  val the_const_type = Consts.the_type o consts_of;
    1.22  val const_type = try o the_const_type;
    1.23  val const_monomorphic = Consts.is_monomorphic o consts_of;
    1.24 -val const_syntax_name = Consts.syntax_name o consts_of;
    1.25  val const_typargs = Consts.typargs o consts_of;
    1.26  val const_instance = Consts.instance o consts_of;
    1.27  
    1.28 @@ -299,7 +297,7 @@
    1.29  val intern_typ = typ_mapping intern_class intern_type;
    1.30  val extern_typ = typ_mapping extern_class extern_type;
    1.31  val intern_term = term_mapping intern_class intern_type intern_const;
    1.32 -fun extern_term h = term_mapping extern_class extern_type (K h);
    1.33 +val extern_term = term_mapping extern_class extern_type (fn _ => fn c => Syntax.constN ^ c);
    1.34  val intern_tycons = typ_mapping (K I) intern_type;
    1.35  
    1.36  end;
    1.37 @@ -486,7 +484,10 @@
    1.38  fun notation add mode args thy =
    1.39    let
    1.40      val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram;
    1.41 -    fun const_syntax (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
    1.42 +    fun const_syntax (Const (c, _), mx) =
    1.43 +          (case try (Consts.type_scheme (consts_of thy)) c of
    1.44 +            SOME T => SOME (Syntax.constN ^ c, T, mx)
    1.45 +          | NONE => NONE)
    1.46        | const_syntax _ = NONE;
    1.47    in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end;
    1.48  
    1.49 @@ -495,14 +496,14 @@
    1.50  
    1.51  local
    1.52  
    1.53 -fun gen_add_consts parse_typ authentic raw_args thy =
    1.54 +fun gen_add_consts parse_typ raw_args thy =
    1.55    let
    1.56      val ctxt = ProofContext.init thy;
    1.57      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    1.58      fun prep (b, raw_T, mx) =
    1.59        let
    1.60          val c = full_name thy b;
    1.61 -        val c_syn = if authentic then Syntax.constN ^ c else Name.of_binding b;
    1.62 +        val c_syn = Syntax.constN ^ c;
    1.63          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.64            cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
    1.65          val T' = Logic.varifyT T;
    1.66 @@ -510,20 +511,20 @@
    1.67      val args = map prep raw_args;
    1.68    in
    1.69      thy
    1.70 -    |> map_consts (fold (Consts.declare authentic (naming_of thy) o #1) args)
    1.71 +    |> map_consts (fold (Consts.declare (naming_of thy) o #1) args)
    1.72      |> add_syntax_i (map #2 args)
    1.73      |> pair (map #3 args)
    1.74    end;
    1.75  
    1.76  in
    1.77  
    1.78 -fun add_consts args = snd o gen_add_consts Syntax.parse_typ false args;
    1.79 -fun add_consts_i args = snd o gen_add_consts (K I) false args;
    1.80 +fun add_consts args = snd o gen_add_consts Syntax.parse_typ args;
    1.81 +fun add_consts_i args = snd o gen_add_consts (K I) args;
    1.82  
    1.83  fun declare_const ((b, T), mx) thy =
    1.84    let
    1.85      val pos = Binding.pos_of b;
    1.86 -    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true [(b, T, mx)] thy;
    1.87 +    val ([const as Const (c, _)], thy') = gen_add_consts (K I) [(b, T, mx)] thy;
    1.88      val _ = Position.report (Markup.const_decl c) pos;
    1.89    in (const, thy') end;
    1.90