src/HOL/UNITY/Extend.ML

 qed "h_f_g_eq";
 
 
 (** A sequence of proof steps borrowed from Provers/split_paired_all.ML **)
 
-val cT = TFree ("'c", ["term"]);
+val cT = TFree ("'c", HOLogic.typeS);
 
 (* "PROP P x == PROP P (h (f x, g x))" *)
 val lemma1 = Thm.combination
   (Thm.reflexive (cterm_of (sign_of thy) (Free ("P", cT --> propT))))
   (Drule.unvarify (h_f_g_eq RS sym RS eq_reflection));