# HG changeset patch # User wenzelm # Date 1268686655 -3600 # Node ID 76b2a53a199d2a1d4ead1882b637462970067c89 # Parent 7adb03f27b28be8cad2a7b147a7cf4c846a2436c moved old Sign.intern_term to the place where it is still used; diff -r 7adb03f27b28 -r 76b2a53a199d src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 15 20:27:23 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 15 21:57:35 2010 +0100 @@ -50,9 +50,29 @@ (* ----- general proof facilities ------------------------------------------- *) +local + +fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts) + | map_typ f _ (TFree (x, S)) = TFree (x, map f S) + | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S); + +fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T) + | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T) + | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T) + | map_term _ _ _ (t as Bound _) = t + | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t) + | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u; + +in + +fun intern_term thy = + map_term (Sign.intern_class thy) (Sign.intern_type thy) (Sign.intern_const thy); + +end; + fun legacy_infer_term thy t = let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy) - in singleton (Syntax.check_terms ctxt) (Sign.intern_term thy t) end; + in singleton (Syntax.check_terms ctxt) (intern_term thy t) end; fun pg'' thy defs t tacs = let @@ -451,7 +471,7 @@ local fun legacy_infer_term thy t = - singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); + singleton (Syntax.check_terms (ProofContext.init thy)) (intern_term thy t); fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); fun infer_props thy = map (apsnd (legacy_infer_prop thy)); fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x); diff -r 7adb03f27b28 -r 76b2a53a199d src/Pure/sign.ML --- a/src/Pure/sign.ML Mon Mar 15 20:27:23 2010 +0100 +++ b/src/Pure/sign.ML Mon Mar 15 21:57:35 2010 +0100 @@ -56,7 +56,6 @@ val extern_type: theory -> string -> xstring val intern_const: theory -> xstring -> string val extern_const: theory -> string -> xstring - val intern_term: theory -> term -> term val arity_number: theory -> string -> int val arity_sorts: theory -> string -> sort -> sort list val certify_class: theory -> class -> class @@ -247,25 +246,6 @@ val intern_const = Name_Space.intern o const_space; val extern_const = Name_Space.extern o const_space; -local - -fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts) - | map_typ f _ (TFree (x, S)) = TFree (x, map f S) - | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S); - -fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T) - | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T) - | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T) - | map_term _ _ _ (t as Bound _) = t - | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t) - | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u; - -in - -fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy); - -end; - (** certify entities **) (*exception TYPE*)