moved old Sign.intern_term to the place where it is still used;
authorwenzelm
Mon Mar 15 21:57:35 2010 +0100 (2010-03-15 ago)
changeset 3580076b2a53a199d
parent 35799 7adb03f27b28
child 35801 952308389b8b
moved old Sign.intern_term to the place where it is still used;
src/HOLCF/Tools/Domain/domain_theorems.ML
src/Pure/sign.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 15 20:27:23 2010 +0100
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 15 21:57:35 2010 +0100
     1.3 @@ -50,9 +50,29 @@
     1.4  
     1.5  (* ----- general proof facilities ------------------------------------------- *)
     1.6  
     1.7 +local
     1.8 +
     1.9 +fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
    1.10 +  | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
    1.11 +  | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
    1.12 +
    1.13 +fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
    1.14 +  | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
    1.15 +  | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
    1.16 +  | map_term _ _ _ (t as Bound _) = t
    1.17 +  | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
    1.18 +  | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
    1.19 +
    1.20 +in
    1.21 +
    1.22 +fun intern_term thy =
    1.23 +  map_term (Sign.intern_class thy) (Sign.intern_type thy) (Sign.intern_const thy);
    1.24 +
    1.25 +end;
    1.26 +
    1.27  fun legacy_infer_term thy t =
    1.28    let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy)
    1.29 -  in singleton (Syntax.check_terms ctxt) (Sign.intern_term thy t) end;
    1.30 +  in singleton (Syntax.check_terms ctxt) (intern_term thy t) end;
    1.31  
    1.32  fun pg'' thy defs t tacs =
    1.33    let
    1.34 @@ -451,7 +471,7 @@
    1.35  local
    1.36  
    1.37    fun legacy_infer_term thy t =
    1.38 -      singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
    1.39 +      singleton (Syntax.check_terms (ProofContext.init thy)) (intern_term thy t);
    1.40    fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
    1.41    fun infer_props thy = map (apsnd (legacy_infer_prop thy));
    1.42    fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
     2.1 --- a/src/Pure/sign.ML	Mon Mar 15 20:27:23 2010 +0100
     2.2 +++ b/src/Pure/sign.ML	Mon Mar 15 21:57:35 2010 +0100
     2.3 @@ -56,7 +56,6 @@
     2.4    val extern_type: theory -> string -> xstring
     2.5    val intern_const: theory -> xstring -> string
     2.6    val extern_const: theory -> string -> xstring
     2.7 -  val intern_term: theory -> term -> term
     2.8    val arity_number: theory -> string -> int
     2.9    val arity_sorts: theory -> string -> sort -> sort list
    2.10    val certify_class: theory -> class -> class
    2.11 @@ -247,25 +246,6 @@
    2.12  val intern_const = Name_Space.intern o const_space;
    2.13  val extern_const = Name_Space.extern o const_space;
    2.14  
    2.15 -local
    2.16 -
    2.17 -fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
    2.18 -  | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
    2.19 -  | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
    2.20 -
    2.21 -fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
    2.22 -  | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
    2.23 -  | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
    2.24 -  | map_term _ _ _ (t as Bound _) = t
    2.25 -  | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
    2.26 -  | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
    2.27 -
    2.28 -in
    2.29 -
    2.30 -fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy);
    2.31 -
    2.32 -end;
    2.33 -
    2.34  
    2.35  
    2.36  (** certify entities **)    (*exception TYPE*)