| changeset 43545 | 1cf2256f1b07 |
| parent 43303 | c4ea897a5326 |
| child 43626 | a867ebb12209 |
--- 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"