src/Pure/Proof/proof_syntax.ML

--- a/src/Pure/Proof/proof_syntax.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -128,7 +128,7 @@
     val thms = PureThy.all_thms_of thy;
     val axms = Theory.all_axioms_of thy;
 
-    fun mk_term t = (if ty then I else map_term_types (K dummyT))
+    fun mk_term t = (if ty then I else map_types (K dummyT))
       (Term.no_dummy_patterns t);
 
     fun prf_of [] (Bound i) = PBound i