| changeset 52034 | 11b48e7a4e7e |
| parent 52031 | 9a9238342963 |
| child 52125 | ac7830871177 |
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu May 16 14:27:43 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu May 16 14:58:30 2013 +0200 @@ -78,7 +78,7 @@ in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s - | term_name' t = "" + | term_name' _ = "" fun lambda' v = Term.lambda_name (term_name' v, v)