src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 56638 092a306bcc3d
parent 56487 961b34963fa4
child 56640 0a35354137a5
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 23 10:23:26 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 23 10:23:26 2014 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  open BNF_FP_N2M_Tactics
     1.5  
     1.6  fun force_typ ctxt T =
     1.7 -  map_types Type_Infer.paramify_vars
     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);