author | wenzelm |
Sat, 25 Jun 2011 15:02:12 +0200 | |
changeset 43545 | 1cf2256f1b07 |
parent 43544 | 6b95bcc5c2da |
child 43546 | 6629e2dedb00 |
--- a/src/HOL/Tools/Metis/metis_tactics.ML Sat Jun 25 14:28:43 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Sat Jun 25 15:02:12 2011 +0200 @@ -33,7 +33,7 @@ open Metis_Translate open Metis_Reconstruct -val metisN = Binding.qualified_name_of @{binding metis} +val metisN = "metis" val full_typesN = "full_types" val partial_typesN = "partial_types"