src/Pure/Isar/isar_syn.ML

--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 07 14:25:48 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 07 20:42:13 2004 +0200
@@ -359,8 +359,7 @@
 
 val instantiateP =
   OuterSyntax.command "instantiate" "instantiate locale" K.prf_decl
-    (P.name --| P.$$$ ":" -- P.xname
-(*    (P.xname -- (P.$$$ "[" |-- P.name --| P.$$$ "]") *)
+    (P.opt_thm_name ":" -- P.xname
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.instantiate_locale)));