src/HOL/Tools/ATP/recon_translate_proof.ML
changeset 15794 5de27a5fc5ed
parent 15789 4cb16144c81b
child 15919 b30a35432f5a
     1.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Thu Apr 21 18:56:03 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Thu Apr 21 18:57:18 2005 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4  (*******************************************)
     1.5  
     1.6  fun mksubstlist [] sublist = sublist
     1.7 -   |mksubstlist ((a,b)::rest) sublist = let val vartype = type_of b 
     1.8 +   |mksubstlist ((a, (_, b)) :: rest) sublist = let val vartype = type_of b 
     1.9                                            val avar = Var(a,vartype)
    1.10                                            val newlist = ((avar,b)::sublist) in
    1.11                                            mksubstlist rest newlist