# HG changeset patch
# User blanchet
# Date 1449005077 -3600
# Node ID a20048c788913580c2c01df4125032cdb730aa52
# Parent  2cd36f4c5d6554309bbbfe371e9a77bee5a65a0e
removed needless ML function

diff -r 2cd36f4c5d65 -r a20048c78891 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Tue Dec 01 22:21:40 2015 +0100
+++ b/src/HOL/Library/refute.ML	Tue Dec 01 22:24:37 2015 +0100
@@ -375,7 +375,6 @@
     end
 
 val close_form = ATP_Util.close_form
-val monomorphic_term = ATP_Util.monomorphic_term
 val specialize_type = ATP_Util.specialize_type
 
 (* ------------------------------------------------------------------------- *)
@@ -451,7 +450,7 @@
             if s=s' then
               let
                 val typeSubs = Sign.typ_match thy (T', T) Vartab.empty
-                val ax'      = monomorphic_term typeSubs ax
+                val ax'      = Envir.subst_term_types typeSubs ax
                 val rhs      = norm_rhs ax'
               in
                 SOME (axname, rhs)
@@ -495,7 +494,7 @@
                   val T'' = domain_type (domain_type T')
                   val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty
                 in
-                  SOME (axname, monomorphic_term typeSubs ax)
+                  SOME (axname, Envir.subst_term_types typeSubs ax)
                 end
             | NONE => get_typedef_ax axioms
           end handle ERROR _         => get_typedef_ax axioms
@@ -669,7 +668,7 @@
         val monomorphic_class_axioms = map (fn (axname, ax) =>
           (case Term.add_tvars ax [] of
             [] => (axname, ax)
-          | [(idx, S)] => (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
+          | [(idx, S)] => (axname, Envir.subst_term_types (Vartab.make [(idx, (S, T))]) ax)
           | _ =>
             raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^
               Syntax.string_of_term ctxt ax ^
diff -r 2cd36f4c5d65 -r a20048c78891 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Dec 01 22:21:40 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Dec 01 22:24:37 2015 +0100
@@ -1715,7 +1715,7 @@
       fun specialize_helper t T =
         if unmangled_s = app_op_name then
           let val tyenv = Sign.typ_match thy (alpha_to_beta, domain_type T) Vartab.empty in
-            monomorphic_term tyenv t
+            Envir.subst_term_types tyenv t
           end
         else
           specialize_type thy (invert_const unmangled_s, T) t
diff -r 2cd36f4c5d65 -r a20048c78891 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Dec 01 22:21:40 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Dec 01 22:24:37 2015 +0100
@@ -39,7 +39,6 @@
   val hol_close_form_prefix : string
   val hol_close_form : term -> term
   val hol_open_form : (string -> string) -> term -> term
-  val monomorphic_term : Type.tyenv -> term -> term
   val eta_expand : typ list -> term -> int -> term
   val cong_extensionalize_term : Proof.context -> term -> term
   val abs_extensionalize_term : Proof.context -> term -> term
@@ -324,12 +323,6 @@
      | NONE => t)
   | hol_open_form _ t = t
 
-fun monomorphic_term subst =
-  map_types (map_type_tvar (fn v =>
-      case Type.lookup subst v of
-        SOME typ => typ
-      | NONE => TVar v))
-
 fun eta_expand _ t 0 = t
   | eta_expand Ts (Abs (s, T, t')) n =
     Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
@@ -395,7 +388,7 @@
       | subst_for _ = NONE
   in
     (case subst_for t of
-      SOME subst => monomorphic_term subst t
+      SOME subst => Envir.subst_term_types subst t
     | NONE => raise Type.TYPE_MATCH)
   end
 
diff -r 2cd36f4c5d65 -r a20048c78891 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 01 22:21:40 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 01 22:24:37 2015 +0100
@@ -1525,8 +1525,8 @@
           ys |> (if AList.defined (op =) ys T' then
                    I
                  else
-                   cons (T', monomorphic_term (Sign.typ_match thy (T', T)
-                                                              Vartab.empty) t)
+                   cons (T', Envir.subst_term_types (Sign.typ_match thy (T', T)
+                     Vartab.empty) t)
                    handle Type.TYPE_MATCH => I
                         | TERM _ =>
                           if slack then
diff -r 2cd36f4c5d65 -r a20048c78891 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 01 22:21:40 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 01 22:24:37 2015 +0100
@@ -1031,7 +1031,7 @@
           map (fn t => case Term.add_tvars t [] of
                          [] => t
                        | [(x, S)] =>
-                         monomorphic_term (Vartab.make [(x, (S, T))]) t
+                         Envir.subst_term_types (Vartab.make [(x, (S, T))]) t
                        | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
                                           \add_axioms_for_sort", [t]))
               class_axioms
diff -r 2cd36f4c5d65 -r a20048c78891 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Dec 01 22:21:40 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Dec 01 22:24:37 2015 +0100
@@ -65,7 +65,6 @@
   val varify_and_instantiate_type_global : theory -> typ -> typ -> typ -> typ
   val is_of_class_const : theory -> string * typ -> bool
   val get_class_def : theory -> string -> (string * term) option
-  val monomorphic_term : Type.tyenv -> term -> term
   val specialize_type : theory -> string * typ -> term -> term
   val eta_expand : typ list -> term -> int -> term
   val DETERM_TIMEOUT : Time.time -> tactic -> tactic
@@ -270,7 +269,6 @@
       (AList.lookup (op =) (Theory.all_axioms_of thy) axname)
   end;
 
-val monomorphic_term = ATP_Util.monomorphic_term
 val specialize_type = ATP_Util.specialize_type
 val eta_expand = ATP_Util.eta_expand