# HG changeset patch
# User haftmann
# Date 1177060907 -7200
# Node ID 17bc6af2011edf6aef5d541320a3f04546255899
# Parent  5cbe966d67a2196a2c53fbf8ac0cf78437de141e
moved axclass module closer to core system

diff -r 5cbe966d67a2 -r 17bc6af2011e src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 20 11:21:42 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 20 11:21:47 2007 +0200
@@ -224,7 +224,7 @@
                        (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
                         HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
       in
-          AxClass.define_class_i (cl_name, ["HOL.type"]) []
+          AxClass.define_class (cl_name, ["HOL.type"]) []
                 [((cl_name ^ "1", [Simplifier.simp_add]), [axiom1]),
                  ((cl_name ^ "2", []), [axiom2]),                           
                  ((cl_name ^ "3", []), [axiom3])] thy                          
@@ -273,7 +273,7 @@
           val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
 
        in  
-        AxClass.define_class_i (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
+        AxClass.define_class (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
        end) ak_names_types thy8; 
 	 
      (* proves that every fs_<ak>-type together with <ak>-type   *)
@@ -322,7 +322,7 @@
 			   (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
                                            cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
 	       in  
-		 AxClass.define_class_i (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
+		 AxClass.define_class (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
 	       end) ak_names_types thy) ak_names_types thy12;
 
         (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)
diff -r 5cbe966d67a2 -r 17bc6af2011e src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Apr 20 11:21:42 2007 +0200
+++ b/src/Pure/axclass.ML	Fri Apr 20 11:21:47 2007 +0200
@@ -21,11 +21,8 @@
   val add_arity: thm -> theory -> theory
   val prove_classrel: class * class -> tactic -> theory -> theory
   val prove_arity: string * sort list * sort -> tactic -> theory -> theory
-  val define_class: bstring * xstring list -> string list ->
-    ((bstring * Attrib.src list) * string list) list -> theory -> class * theory
-  val define_class_i: bstring * class list -> string list ->
+  val define_class: bstring * class list -> string list ->
     ((bstring * attribute list) * term list) list -> theory -> class * theory
-  val read_param: theory -> string -> string
   val axiomatize_class: bstring * xstring list -> theory -> theory
   val axiomatize_class_i: bstring * class list -> theory -> theory
   val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
@@ -270,18 +267,7 @@
 
 (** class definitions **)
 
-fun read_param thy raw_t =
-  let
-    val t = Sign.read_term thy raw_t
-  in case try dest_Const t
-   of SOME (c, _) => c
-    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
-  end;
-
-local
-
-fun def_class prep_class prep_att prep_param prep_propp
-    (bclass, raw_super) raw_params raw_specs thy =
+fun define_class (bclass, raw_super) params raw_specs thy =
   let
     val ctxt = ProofContext.init thy;
     val pp = ProofContext.pp ctxt;
@@ -291,7 +277,7 @@
 
     val bconst = Logic.const_of_class bclass;
     val class = Sign.full_name thy bclass;
-    val super = map (prep_class thy) raw_super |> Sign.certify_sort thy;
+    val super = Sign.certify_sort thy raw_super;
 
     fun prep_axiom t =
       (case Term.add_tfrees t [] of
@@ -305,9 +291,10 @@
       |> map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
       |> Logic.close_form;
 
-    val axiomss = prep_propp (ctxt, map (map (rpair []) o snd) raw_specs)
+    (*FIXME is ProofContext.cert_propp really neccessary?*)
+    val axiomss = ProofContext.cert_propp (ctxt, map (map (rpair []) o snd) raw_specs)
       |> snd |> map (map (prep_axiom o fst));
-    val name_atts = Attrib.map_specs (prep_att thy) raw_specs |> map fst;
+    val name_atts = map fst raw_specs;
 
 
     (* definition *)
@@ -336,7 +323,6 @@
 
     (* params *)
 
-    val params = map (prep_param thy) raw_params;
     val params_typs = map (fn param =>
       let
         val ty = Sign.the_const_type thy param;
@@ -361,13 +347,6 @@
 
   in (class, result_thy) end;
 
-in
-
-val define_class = def_class Sign.read_class Attrib.attribute read_param ProofContext.read_propp;
-val define_class_i = def_class Sign.certify_class (K I) (K I) ProofContext.cert_propp;
-
-end;
-
 
 
 (** axiomatizations **)