src/Pure/Proof/proof_syntax.ML
changeset 20548 8ef25fe585a8
parent 19618 9050a3b01e62
child 21056 2cfe839e8d58
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Sep 15 22:56:08 2006 +0200
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Sep 15 22:56:13 2006 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4      val thms = PureThy.all_thms_of thy;
     1.5      val axms = Theory.all_axioms_of thy;
     1.6  
     1.7 -    fun mk_term t = (if ty then I else map_term_types (K dummyT))
     1.8 +    fun mk_term t = (if ty then I else map_types (K dummyT))
     1.9        (Term.no_dummy_patterns t);
    1.10  
    1.11      fun prf_of [] (Bound i) = PBound i