src/HOL/Tools/refute.ML
changeset 36555 8ff45c2076da
parent 36374 19c0c4b8b445
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Apr 29 01:11:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Apr 29 01:17:14 2010 +0200
     1.3 @@ -70,8 +70,6 @@
     1.4    val is_IDT_constructor : theory -> string * typ -> bool
     1.5    val is_IDT_recursor : theory -> string * typ -> bool
     1.6    val is_const_of_class: theory -> string * typ -> bool
     1.7 -  val monomorphic_term : Type.tyenv -> term -> term
     1.8 -  val specialize_type : theory -> (string * typ) -> term -> term
     1.9    val string_of_typ : typ -> string
    1.10    val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
    1.11  end;  (* signature REFUTE *)
    1.12 @@ -449,57 +447,8 @@
    1.13        Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
    1.14    end;
    1.15  
    1.16 -(* ------------------------------------------------------------------------- *)
    1.17 -(* monomorphic_term: applies a type substitution 'typeSubs' for all type     *)
    1.18 -(*                   variables in a term 't'                                 *)
    1.19 -(* ------------------------------------------------------------------------- *)
    1.20 -
    1.21 -  (* Type.tyenv -> Term.term -> Term.term *)
    1.22 -
    1.23 -  fun monomorphic_term typeSubs t =
    1.24 -    map_types (map_type_tvar
    1.25 -      (fn v =>
    1.26 -        case Type.lookup typeSubs v of
    1.27 -          NONE =>
    1.28 -          (* schematic type variable not instantiated *)
    1.29 -          raise REFUTE ("monomorphic_term",
    1.30 -            "no substitution for type variable " ^ fst (fst v) ^
    1.31 -            " in term " ^ Syntax.string_of_term_global Pure.thy t)
    1.32 -        | SOME typ =>
    1.33 -          typ)) t;
    1.34 -
    1.35 -(* ------------------------------------------------------------------------- *)
    1.36 -(* specialize_type: given a constant 's' of type 'T', which is a subterm of  *)
    1.37 -(*                  't', where 't' has a (possibly) more general type, the   *)
    1.38 -(*                  schematic type variables in 't' are instantiated to      *)
    1.39 -(*                  match the type 'T' (may raise Type.TYPE_MATCH)           *)
    1.40 -(* ------------------------------------------------------------------------- *)
    1.41 -
    1.42 -  (* theory -> (string * Term.typ) -> Term.term -> Term.term *)
    1.43 -
    1.44 -  fun specialize_type thy (s, T) t =
    1.45 -  let
    1.46 -    fun find_typeSubs (Const (s', T')) =
    1.47 -      if s=s' then
    1.48 -        SOME (Sign.typ_match thy (T', T) Vartab.empty)
    1.49 -          handle Type.TYPE_MATCH => NONE
    1.50 -      else
    1.51 -        NONE
    1.52 -      | find_typeSubs (Free _)           = NONE
    1.53 -      | find_typeSubs (Var _)            = NONE
    1.54 -      | find_typeSubs (Bound _)          = NONE
    1.55 -      | find_typeSubs (Abs (_, _, body)) = find_typeSubs body
    1.56 -      | find_typeSubs (t1 $ t2)          =
    1.57 -      (case find_typeSubs t1 of SOME x => SOME x
    1.58 -                              | NONE   => find_typeSubs t2)
    1.59 -  in
    1.60 -    case find_typeSubs t of
    1.61 -      SOME typeSubs =>
    1.62 -      monomorphic_term typeSubs t
    1.63 -    | NONE =>
    1.64 -      (* no match found - perhaps due to sort constraints *)
    1.65 -      raise Type.TYPE_MATCH
    1.66 -  end;
    1.67 +val monomorphic_term = Sledgehammer_Util.monomorphic_term
    1.68 +val specialize_type = Sledgehammer_Util.specialize_type
    1.69  
    1.70  (* ------------------------------------------------------------------------- *)
    1.71  (* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that   *)