# HG changeset patch
# User haftmann
# Date 1158672148 -7200
# Node ID 3e1caf5a07c69bee7ee1d84179cdd3f73f1d5526
# Parent  6d75e02ed285a15ffbb7a5e5cd592450f2112e30
classical arity syntax

diff -r 6d75e02ed285 -r 3e1caf5a07c6 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Tue Sep 19 15:22:26 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Tue Sep 19 15:22:28 2006 +0200
@@ -11,11 +11,10 @@
     -> Proof.context * theory
   val class_i: bstring -> class list -> Element.context_i Locale.element list -> theory
     -> Proof.context * theory
-  (*FIXME: in _i variants, bstring should be bstring option*)
-  val instance_arity: ((xstring * string list) * string) list
+  val instance_arity: ((bstring * string list) * string) list
     -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
     -> theory -> Proof.state
-  val instance_arity_i: ((string * sort list) * sort) list
+  val instance_arity_i: ((bstring * sort list) * sort) list
     -> bstring * attribute list -> ((bstring * attribute list) * term) list
     -> theory -> Proof.state
   val prove_instance_arity: (thm list -> tactic) -> ((string * sort list) * sort) list
@@ -332,7 +331,7 @@
           fold (add_global_constraint v name_axclass) mapp_this
     #> add_class_data (name_locale, (name_locale, name_axclass, v, mapp_this,
          map (fst o fst) loc_axioms))
-    #> prove_interpretation_i (NameSpace.base name_locale, [])
+    #> prove_interpretation_i (bname, [])
           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this)))
           ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
     #> pair ctxt
@@ -441,7 +440,7 @@
             ((snd o the_class_data thy) class) tyco) (the_ancestry thy sort)) arities;
       in if bind then
         thy
-        |> PureThy.note_thmss_i PureThy.internalK [((name, atts), [(thms, [])])]
+        |> PureThy.note_thmss_i (*qualified*) PureThy.internalK [((name, atts), [(thms, [])])]
         |> snd
       else
         thy
@@ -579,10 +578,8 @@
 val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
 val class_bodyP = P.!!! (Scan.repeat1 P.locale_element);
 
-val inst =
-  (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 P.sort --| P.$$$ ")")) [] -- P.xname --| P.$$$ "::" -- P.sort)
-    >> (fn ((asorts, tyco), sort) => ((tyco, asorts), sort))
-  || (P.xname --| P.$$$ "::" -- P.!!! P.arity)
+val parse_arity =
+  (P.xname --| P.$$$ "::" -- P.!!! P.arity)
     >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
 
 val classP =
@@ -598,7 +595,7 @@
 val instanceP =
   OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> wrap_add_instance_sort
-      || P.opt_thm_name ":" -- (P.and_list1 inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop))
+      || P.opt_thm_name ":" -- (P.and_list1 parse_arity -- Scan.repeat (P.opt_thm_name ":" -- P.prop))
            >> (fn (("", []), ([((tyco, asorts), sort)], [])) => axclass_instance_arity I [(tyco, asorts, sort)]
                 | (natts, (arities, defs)) => instance_arity arities natts defs)
     ) >> (Toplevel.print oo Toplevel.theory_to_proof));