src/Pure/sign.ML
changeset 35800 76b2a53a199d
parent 35680 897740382442
child 35801 952308389b8b
     1.1 --- a/src/Pure/sign.ML	Mon Mar 15 20:27:23 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Mar 15 21:57:35 2010 +0100
     1.3 @@ -56,7 +56,6 @@
     1.4    val extern_type: theory -> string -> xstring
     1.5    val intern_const: theory -> xstring -> string
     1.6    val extern_const: theory -> string -> xstring
     1.7 -  val intern_term: theory -> term -> term
     1.8    val arity_number: theory -> string -> int
     1.9    val arity_sorts: theory -> string -> sort -> sort list
    1.10    val certify_class: theory -> class -> class
    1.11 @@ -247,25 +246,6 @@
    1.12  val intern_const = Name_Space.intern o const_space;
    1.13  val extern_const = Name_Space.extern o const_space;
    1.14  
    1.15 -local
    1.16 -
    1.17 -fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
    1.18 -  | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
    1.19 -  | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
    1.20 -
    1.21 -fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
    1.22 -  | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
    1.23 -  | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
    1.24 -  | map_term _ _ _ (t as Bound _) = t
    1.25 -  | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
    1.26 -  | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
    1.27 -
    1.28 -in
    1.29 -
    1.30 -fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy);
    1.31 -
    1.32 -end;
    1.33 -
    1.34  
    1.35  
    1.36  (** certify entities **)    (*exception TYPE*)