refined Variable.declare_const;
authorwenzelm
Wed Nov 07 16:42:58 2007 +0100 (2007-11-07)
changeset 25326e417a7236125
parent 25325 0659c05cc107
child 25327 c65608a84919
refined Variable.declare_const;
removed obsolete Sign.read_tyname/const (cf. ProofContext);
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Wed Nov 07 16:42:57 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Nov 07 16:42:58 2007 +0100
     1.3 @@ -637,7 +637,7 @@
     1.4      val consts = ProofContext.consts_of ctxt;
     1.5      fun declare_const (c, _) =
     1.6        let val b = Sign.base_name c
     1.7 -      in if Consts.intern consts b = c then Variable.declare_const b else I end;
     1.8 +      in Consts.intern consts b = c ? Variable.declare_const (b, c) end;
     1.9      val typargs = Consts.typargs consts;
    1.10      fun check_const (c, ty) (t, (_, typidx)) = ((nth (typargs (c, ty)) typidx), t);
    1.11      fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c
    1.12 @@ -804,7 +804,7 @@
    1.13            #>> Element.Fixes
    1.14        | fork_syntax x = pair x;
    1.15      val (elems, global_syn) = fold_map fork_syntax elems_syn [];
    1.16 -    fun globalize (c, ty) = 
    1.17 +    fun globalize (c, ty) =
    1.18        ((c, Term.map_type_tfree (K (TFree (Name.aT, base_sort))) ty),
    1.19          (the_default NoSyn o AList.lookup (op =) global_syn) c);
    1.20      fun extract_params thy =
    1.21 @@ -851,9 +851,11 @@
    1.22      |> pair class
    1.23    end;
    1.24  
    1.25 +fun read_const thy = #1 o Term.dest_Const o ProofContext.read_const (ProofContext.init thy);
    1.26 +
    1.27  in
    1.28  
    1.29 -val class_cmd = gen_class read_class_spec ((#1 o Term.dest_Const) oo Sign.read_const);
    1.30 +val class_cmd = gen_class read_class_spec read_const;
    1.31  val class = gen_class check_class_spec (K I);
    1.32  
    1.33  end; (*local*)