# HG changeset patch
# User wenzelm
# Date 958912527 -7200
# Node ID fb1436ca3b2e8ac1148a540029184ce70a2c6e76
# Parent  c80aba8c1d5ecad2abfd5fe54201fed6a74fd9dc
adapted to inner syntax of sorts;

diff -r c80aba8c1d5e -r fb1436ca3b2e src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sun May 21 14:35:27 2000 +0200
@@ -28,14 +28,14 @@
   val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
   val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
   val add_classrel_i: (class * class) * Comment.text -> theory -> theory
-  val add_defsort: xsort * Comment.text -> theory -> theory
+  val add_defsort: string * Comment.text -> theory -> theory
   val add_defsort_i: sort * Comment.text -> theory -> theory
   val add_nonterminals: (bstring * Comment.text) list -> theory -> theory
   val add_tyabbrs: ((bstring * string list * string * mixfix) * Comment.text) list
     -> theory -> theory
   val add_tyabbrs_i: ((bstring * string list * typ * mixfix) * Comment.text) list
     -> theory -> theory
-  val add_arities: ((xstring * xsort list * xsort) * Comment.text) list -> theory -> theory
+  val add_arities: ((xstring * string list * string) * Comment.text) list -> theory -> theory
   val add_arities_i: ((string * sort list * sort) * Comment.text) list -> theory -> theory
   val add_typedecl: (bstring * string list * mixfix) * Comment.text -> theory -> theory
   val add_consts: ((bstring * string * mixfix) * Comment.text) list -> theory -> theory
diff -r c80aba8c1d5e -r fb1436ca3b2e src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Sun May 21 14:35:27 2000 +0200
@@ -42,9 +42,9 @@
   val comment: token list -> Comment.text * token list
   val marg_comment: token list -> Comment.text * token list
   val interest: token list -> Comment.interest * token list
-  val sort: token list -> xsort * token list
-  val arity: token list -> (xsort list * xsort) * token list
-  val simple_arity: token list -> (xsort list * xclass) * token list
+  val sort: token list -> string * token list
+  val arity: token list -> (string list * string) * token list
+  val simple_arity: token list -> (string list * xclass) * token list
   val type_args: token list -> string list * token list
   val typ: token list -> string * token list
   val opt_infix: token list -> Syntax.mixfix * token list
@@ -175,14 +175,13 @@
 
 (* sorts and arities *)
 
-val sort =
-  xname >> single || $$$ "{" |-- !!! (list xname --| $$$ "}");
+val sort = group "sort" xname;
 
 fun gen_arity cod =
   Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- cod;
 
 val arity = gen_arity sort;
-val simple_arity = gen_arity name;
+val simple_arity = gen_arity xname;
 
 
 (* types *)
@@ -266,7 +265,6 @@
   ((Scan.repeat1
     (Scan.repeat1 (atom_arg is_symid blk) ||
       paren_args "(" ")" (args is_symid) ||
-      paren_args "{" "}" (args is_symid) ||
       paren_args "[" "]" (args is_symid))) >> flat) x;
 
 
diff -r c80aba8c1d5e -r fb1436ca3b2e src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Sun May 21 14:35:27 2000 +0200
@@ -201,13 +201,9 @@
 
 (* arities *)
 
-val sort =
-  name >> brackets ||
-  "{" $$-- name_list --$$ "}";
-
+val sort = name || "{" $$-- list ident --$$ "}" >> (quote o enclose "{" "}" o commas);
 val sort_list1 = list1 sort >> mk_list;
 
-
 val arity = optional ("(" $$-- !! (sort_list1 --$$")")) "[]" -- sort;
 
 val arity_decls = repeat1 (names1 --$$ "::" -- !! arity)
diff -r c80aba8c1d5e -r fb1436ca3b2e src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/axclass.ML	Sun May 21 14:35:27 2000 +0200
@@ -19,9 +19,9 @@
     -> tactic option -> theory -> theory
   val add_inst_subclass_i: class * class -> string list -> thm list
     -> tactic option -> theory -> theory
-  val add_inst_arity: xstring * xsort list * xclass list -> string list
+  val add_inst_arity: xstring * string list * string -> string list
     -> thm list -> tactic option -> theory -> theory
-  val add_inst_arity_i: string * sort list * class list -> string list
+  val add_inst_arity_i: string * sort list * sort -> string list
     -> thm list -> tactic option -> theory -> theory
   val axclass_tac: thm list -> tactic
   val prove_subclass: theory -> class * class -> thm list
@@ -29,10 +29,10 @@
   val prove_arity: theory -> string * sort list * class -> thm list
     -> tactic option -> thm
   val goal_subclass: theory -> xclass * xclass -> thm list
-  val goal_arity: theory -> xstring * xsort list * xclass -> thm list
+  val goal_arity: theory -> xstring * string list * xclass -> thm list
   val instance_subclass_proof: (xclass * xclass) * Comment.text -> bool -> theory -> ProofHistory.T
   val instance_subclass_proof_i: (class * class) * Comment.text -> bool -> theory -> ProofHistory.T
-  val instance_arity_proof: (xstring * xsort list * xclass) * Comment.text
+  val instance_arity_proof: (xstring * string list * xclass) * Comment.text
     -> bool -> theory -> ProofHistory.T
   val instance_arity_proof_i: (string * sort list * class) * Comment.text
     -> bool -> theory -> ProofHistory.T
@@ -146,7 +146,7 @@
         val (c1, c2) = dest_classrel prop handle TERM _ =>
           raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]);
       in (c1, c2) end;
-  in Theory.add_classrel (map prep_thm thms) thy end;
+  in Theory.add_classrel_i (map prep_thm thms) thy end;
 
 (*theorems expressing arities*)
 fun add_arity_thms thms thy =
@@ -157,7 +157,7 @@
         val (t, ss, c) = dest_arity prop handle TERM _ =>
           raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]);
       in (t, ss, [c]) end;
-  in Theory.add_arities (map prep_thm thms) thy end;
+  in Theory.add_arities_i (map prep_thm thms) thy end;
 
 
 
@@ -357,15 +357,32 @@
 
 (** add proved subclass relations and arities **)
 
-fun intrn_classrel sg c1_c2 =
-  pairself (Sign.intern_class sg) c1_c2;
+(* prepare classes and arities *)
+
+fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
+
+fun cert_classrel sg cc = Library.pairself (Sign.certify_class sg) cc;
+fun read_classrel sg cc = Library.pairself (read_class sg) cc;
 
-fun intrn_arity intrn sg (raw_t, Ss, x) =
-  let val t = Sign.intern_tycon sg raw_t in
-    if Sign.is_type_abbr sg t then error ("Illegal type abbreviation: " ^ quote t)
-    else (t, map (Sign.intern_sort sg) Ss, intrn sg x)
+fun check_tycon sg t =
+  let val {tycons, abbrs, ...} = Type.rep_tsig (Sign.tsig_of sg) in
+    if is_some (Symtab.lookup (abbrs, t)) then
+      error ("Illegal type abbreviation: " ^ quote t)
+    else if is_none (Symtab.lookup (tycons, t)) then
+      error ("Undeclared type constructor: " ^ quote t)
+    else t
   end;
 
+fun prep_arity prep_tycon prep_sort prep_x sg (t, Ss, x) =
+  (check_tycon sg (prep_tycon sg t), map (prep_sort sg) Ss, prep_x sg x);
+
+val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
+val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
+val read_simple_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.intern_class;
+val cert_simple_arity = prep_arity (K I) Sign.certify_sort (K I);
+
+
+(* old-style instance declarations *)
 
 fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy =
   let val c1_c2 = prep_classrel (Theory.sign_of thy) raw_c1_c2 in
@@ -386,10 +403,10 @@
   in add_arity_thms (map prove cs) thy end;
 
 
-val add_inst_subclass = ext_inst_subclass intrn_classrel;
-val add_inst_subclass_i = ext_inst_subclass (K I);
-val add_inst_arity = ext_inst_arity (intrn_arity Sign.intern_sort);
-val add_inst_arity_i = ext_inst_arity (K I);
+val add_inst_subclass = ext_inst_subclass read_classrel;
+val add_inst_subclass_i = ext_inst_subclass cert_classrel;
+val add_inst_arity = ext_inst_arity read_arity;
+val add_inst_arity_i = ext_inst_arity cert_arity;
 
 
 (* make old-style interactive goals *)
@@ -397,8 +414,8 @@
 fun mk_goal mk_prop thy sig_prop =
   Goals.goalw_cterm [] (Thm.cterm_of (Theory.sign_of thy) (mk_prop (Theory.sign_of thy) sig_prop));
 
-val goal_subclass = mk_goal (mk_classrel oo intrn_classrel);
-val goal_arity = mk_goal (mk_arity oo intrn_arity Sign.intern_class);
+val goal_subclass = mk_goal (mk_classrel oo read_classrel);
+val goal_arity = mk_goal (mk_arity oo read_simple_arity);
 
 
 
@@ -411,10 +428,10 @@
   |> IsarThy.theorem_i (("", [inst_attribute add_thms],
     (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
 
-val instance_subclass_proof = inst_proof (mk_classrel oo intrn_classrel) add_classrel_thms;
-val instance_subclass_proof_i = inst_proof (K mk_classrel) add_classrel_thms;
-val instance_arity_proof = inst_proof (mk_arity oo intrn_arity Sign.intern_class) add_arity_thms;
-val instance_arity_proof_i = inst_proof (K mk_arity) add_arity_thms;
+val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;
+val instance_subclass_proof_i = inst_proof (mk_classrel oo cert_classrel) add_classrel_thms;
+val instance_arity_proof = inst_proof (mk_arity oo read_simple_arity) add_arity_thms;
+val instance_arity_proof_i = inst_proof (mk_arity oo cert_simple_arity) add_arity_thms;
 
 
 
diff -r c80aba8c1d5e -r fb1436ca3b2e src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/theory.ML	Sun May 21 14:35:27 2000 +0200
@@ -40,7 +40,7 @@
   val add_classes_i: (bclass * class list) list -> theory -> theory
   val add_classrel: (xclass * xclass) list -> theory -> theory
   val add_classrel_i: (class * class) list -> theory -> theory
-  val add_defsort: xsort -> theory -> theory
+  val add_defsort: string -> theory -> theory
   val add_defsort_i: sort -> theory -> theory
   val add_types: (bstring * int * mixfix) list -> theory -> theory
   val add_nonterminals: bstring list -> theory -> theory
@@ -48,7 +48,7 @@
     -> theory -> theory
   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list
     -> theory -> theory
-  val add_arities: (xstring * xsort list * xsort) list -> theory -> theory
+  val add_arities: (xstring * string list * string) list -> theory -> theory
   val add_arities_i: (string * sort list * sort) list -> theory -> theory
   val add_consts: (bstring * string * mixfix) list -> theory -> theory
   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory