1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu May 05 10:47:33 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu May 05 12:40:48 2011 +0200
     1.3 @@ -570,17 +570,6 @@
     1.4                   "Code_Numeral.code_numeral"] s orelse
     1.5    (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
     1.6  
     1.7 -(* TODO: use "Term_Subst.instantiateT" instead? *)
     1.8 -fun instantiate_type thy T1 T1' T2 =
     1.9 -  Same.commit (Envir.subst_type_same
    1.10 -                   (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
    1.11 -  handle Type.TYPE_MATCH =>
    1.12 -         raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
    1.13 -fun varify_and_instantiate_type ctxt T1 T1' T2 =
    1.14 -  let val thy = Proof_Context.theory_of ctxt in
    1.15 -    instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
    1.16 -  end
    1.17 -
    1.18  fun repair_constr_type ctxt body_T' T =
    1.19    varify_and_instantiate_type ctxt (body_type T) body_T' T
    1.20