src/HOL/Library/refute.ML
changeset 61770 a20048c78891
parent 60924 610794dff23c
child 62519 a564458f94db
     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 ^