src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 62905 52c5a25e0c96
parent 62863 e0b894bba6ff
child 62907 9ad0bac25a84
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 07 17:26:22 2016 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 07 17:56:22 2016 +0200
     1.3 @@ -24,12 +24,6 @@
     1.4  open BNF_Tactics
     1.5  open BNF_FP_N2M_Tactics
     1.6  
     1.7 -fun force_typ ctxt T =
     1.8 -  Term.map_types Type_Infer.paramify_vars
     1.9 -  #> Type.constraint T
    1.10 -  #> Syntax.check_term ctxt
    1.11 -  #> singleton (Variable.polymorphic ctxt);
    1.12 -
    1.13  fun mk_prod_map f g =
    1.14    let
    1.15      val ((fAT, fBT), fT) = `dest_funT (fastype_of f);