| changeset 43085 | 0a2f5b86bdd7 |
| parent 42650 | 552eae49f97d |
| child 43092 | 93ec303e1917 |
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200 @@ -30,6 +30,7 @@ structure Metis_Reconstruct : METIS_RECONSTRUCT = struct +open ATP_Translate open Metis_Translate exception METIS of string * string