removed needless ML function
authorblanchet
Tue Dec 01 22:24:37 2015 +0100 (2015-12-01)
changeset 61770a20048c78891
parent 61769 2cd36f4c5d65
child 61771 acc532690ee1
removed needless ML function
src/HOL/Library/refute.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
     1.1 --- a/src/HOL/Library/refute.ML	Tue Dec 01 22:21:40 2015 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Tue Dec 01 22:24:37 2015 +0100
     1.3 @@ -375,7 +375,6 @@
     1.4      end
     1.5  
     1.6  val close_form = ATP_Util.close_form
     1.7 -val monomorphic_term = ATP_Util.monomorphic_term
     1.8  val specialize_type = ATP_Util.specialize_type
     1.9  
    1.10  (* ------------------------------------------------------------------------- *)
    1.11 @@ -451,7 +450,7 @@
    1.12              if s=s' then
    1.13                let
    1.14                  val typeSubs = Sign.typ_match thy (T', T) Vartab.empty
    1.15 -                val ax'      = monomorphic_term typeSubs ax
    1.16 +                val ax'      = Envir.subst_term_types typeSubs ax
    1.17                  val rhs      = norm_rhs ax'
    1.18                in
    1.19                  SOME (axname, rhs)
    1.20 @@ -495,7 +494,7 @@
    1.21                    val T'' = domain_type (domain_type T')
    1.22                    val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty
    1.23                  in
    1.24 -                  SOME (axname, monomorphic_term typeSubs ax)
    1.25 +                  SOME (axname, Envir.subst_term_types typeSubs ax)
    1.26                  end
    1.27              | NONE => get_typedef_ax axioms
    1.28            end handle ERROR _         => get_typedef_ax axioms
    1.29 @@ -669,7 +668,7 @@
    1.30          val monomorphic_class_axioms = map (fn (axname, ax) =>
    1.31            (case Term.add_tvars ax [] of
    1.32              [] => (axname, ax)
    1.33 -          | [(idx, S)] => (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
    1.34 +          | [(idx, S)] => (axname, Envir.subst_term_types (Vartab.make [(idx, (S, T))]) ax)
    1.35            | _ =>
    1.36              raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^
    1.37                Syntax.string_of_term ctxt ax ^
     2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Dec 01 22:21:40 2015 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Dec 01 22:24:37 2015 +0100
     2.3 @@ -1715,7 +1715,7 @@
     2.4        fun specialize_helper t T =
     2.5          if unmangled_s = app_op_name then
     2.6            let val tyenv = Sign.typ_match thy (alpha_to_beta, domain_type T) Vartab.empty in
     2.7 -            monomorphic_term tyenv t
     2.8 +            Envir.subst_term_types tyenv t
     2.9            end
    2.10          else
    2.11            specialize_type thy (invert_const unmangled_s, T) t
     3.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Tue Dec 01 22:21:40 2015 +0100
     3.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Dec 01 22:24:37 2015 +0100
     3.3 @@ -39,7 +39,6 @@
     3.4    val hol_close_form_prefix : string
     3.5    val hol_close_form : term -> term
     3.6    val hol_open_form : (string -> string) -> term -> term
     3.7 -  val monomorphic_term : Type.tyenv -> term -> term
     3.8    val eta_expand : typ list -> term -> int -> term
     3.9    val cong_extensionalize_term : Proof.context -> term -> term
    3.10    val abs_extensionalize_term : Proof.context -> term -> term
    3.11 @@ -324,12 +323,6 @@
    3.12       | NONE => t)
    3.13    | hol_open_form _ t = t
    3.14  
    3.15 -fun monomorphic_term subst =
    3.16 -  map_types (map_type_tvar (fn v =>
    3.17 -      case Type.lookup subst v of
    3.18 -        SOME typ => typ
    3.19 -      | NONE => TVar v))
    3.20 -
    3.21  fun eta_expand _ t 0 = t
    3.22    | eta_expand Ts (Abs (s, T, t')) n =
    3.23      Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
    3.24 @@ -395,7 +388,7 @@
    3.25        | subst_for _ = NONE
    3.26    in
    3.27      (case subst_for t of
    3.28 -      SOME subst => monomorphic_term subst t
    3.29 +      SOME subst => Envir.subst_term_types subst t
    3.30      | NONE => raise Type.TYPE_MATCH)
    3.31    end
    3.32  
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 01 22:21:40 2015 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 01 22:24:37 2015 +0100
     4.3 @@ -1525,8 +1525,8 @@
     4.4            ys |> (if AList.defined (op =) ys T' then
     4.5                     I
     4.6                   else
     4.7 -                   cons (T', monomorphic_term (Sign.typ_match thy (T', T)
     4.8 -                                                              Vartab.empty) t)
     4.9 +                   cons (T', Envir.subst_term_types (Sign.typ_match thy (T', T)
    4.10 +                     Vartab.empty) t)
    4.11                     handle Type.TYPE_MATCH => I
    4.12                          | TERM _ =>
    4.13                            if slack then
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 01 22:21:40 2015 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 01 22:24:37 2015 +0100
     5.3 @@ -1031,7 +1031,7 @@
     5.4            map (fn t => case Term.add_tvars t [] of
     5.5                           [] => t
     5.6                         | [(x, S)] =>
     5.7 -                         monomorphic_term (Vartab.make [(x, (S, T))]) t
     5.8 +                         Envir.subst_term_types (Vartab.make [(x, (S, T))]) t
     5.9                         | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
    5.10                                            \add_axioms_for_sort", [t]))
    5.11                class_axioms
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Dec 01 22:21:40 2015 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Dec 01 22:24:37 2015 +0100
     6.3 @@ -65,7 +65,6 @@
     6.4    val varify_and_instantiate_type_global : theory -> typ -> typ -> typ -> typ
     6.5    val is_of_class_const : theory -> string * typ -> bool
     6.6    val get_class_def : theory -> string -> (string * term) option
     6.7 -  val monomorphic_term : Type.tyenv -> term -> term
     6.8    val specialize_type : theory -> string * typ -> term -> term
     6.9    val eta_expand : typ list -> term -> int -> term
    6.10    val DETERM_TIMEOUT : Time.time -> tactic -> tactic
    6.11 @@ -270,7 +269,6 @@
    6.12        (AList.lookup (op =) (Theory.all_axioms_of thy) axname)
    6.13    end;
    6.14  
    6.15 -val monomorphic_term = ATP_Util.monomorphic_term
    6.16  val specialize_type = ATP_Util.specialize_type
    6.17  val eta_expand = ATP_Util.eta_expand
    6.18