# 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*)