src/Pure/variable.ML

--- a/src/Pure/variable.ML	Sat Oct 12 12:25:16 2019 +0200
+++ b/src/Pure/variable.ML	Sat Oct 12 13:43:17 2019 +0200
@@ -265,7 +265,8 @@
 
 val declare_typ = declare_term o Logic.mk_type;
 
-val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
+val declare_prf =
+  Proofterm.fold_proof_terms_types declare_internal (declare_internal o Logic.mk_type);
 
 val declare_thm = Thm.fold_terms declare_internal;
 
@@ -616,7 +617,7 @@
 
 fun import_prf is_open prf ctxt =
   let
-    val ts = rev (Proofterm.fold_proof_terms cons (cons o Logic.mk_type) prf []);
+    val ts = rev (Proofterm.fold_proof_terms_types cons (cons o Logic.mk_type) prf []);
     val (insts, ctxt') = import_inst is_open ts ctxt;
   in (Proofterm.instantiate insts prf, ctxt') end;