# HG changeset patch
# User haftmann
# Date 1144332797 -7200
# Node ID 36e537f89585a07c1546ffaecbf22c7b20a59d50
# Parent  f2283f334e427566a02882e494bc1d9e701be1ec
cleanup in typedef/datatype package

diff -r f2283f334e42 -r 36e537f89585 TFL/tfl.ML
--- a/TFL/tfl.ML	Thu Apr 06 16:12:57 2006 +0200
+++ b/TFL/tfl.ML	Thu Apr 06 16:13:17 2006 +0200
@@ -449,7 +449,7 @@
        not simplified. Otherwise large examples (Red-Black trees) are too
        slow.*)
      val case_ss = HOL_basic_ss addcongs
-       DatatypePackage.weak_case_congs_of theory addsimps case_rewrites
+       (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) theory addsimps case_rewrites
      val corollaries' = map (Simplifier.simplify case_ss) corollaries
      val extract = R.CONTEXT_REWRITE_RULE
                      (f, [R], cut_apply, meta_tflCongs@context_congs)
diff -r f2283f334e42 -r 36e537f89585 TFL/thry.ML
--- a/TFL/thry.ML	Thu Apr 06 16:12:57 2006 +0200
+++ b/TFL/thry.ML	Thu Apr 06 16:13:17 2006 +0200
@@ -59,22 +59,21 @@
  * Get information about datatypes
  *---------------------------------------------------------------------------*)
 
-val get_info = Symtab.lookup o DatatypePackage.get_datatypes;
-
-fun match_info thy tname =
-  case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
-      (SOME case_const, SOME constructors) =>
-        SOME {case_const = case_const, constructors = constructors}
+fun match_info thy dtco =
+  case (DatatypePackage.get_datatype thy dtco,
+         DatatypePackage.get_datatype_constrs thy dtco) of
+      (SOME { case_name, ... }, SOME constructors) =>
+        SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
     | _ => NONE;
 
-fun induct_info thy tname = case get_info thy tname of
+fun induct_info thy dtco = case DatatypePackage.get_datatype thy dtco of
         NONE => NONE
       | SOME {nchotomy, ...} =>
           SOME {nchotomy = nchotomy,
-                constructors = valOf (DatatypePackage.constrs_of thy tname)};
+                constructors = (map Const o the o DatatypePackage.get_datatype_constrs thy) dtco};
 
 fun extract_info thy =
- let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
+ let val infos = (map snd o Symtab.dest o DatatypePackage.get_datatypes) thy
  in {case_congs = map (mk_meta_eq o #case_cong) infos,
      case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
  end;
diff -r f2283f334e42 -r 36e537f89585 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Apr 06 16:12:57 2006 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Apr 06 16:13:17 2006 +0200
@@ -2094,7 +2094,7 @@
 	    val tnames = map fst tfrees
 	    val tsyn = mk_syn thy tycname
 	    val typ = (tycname,tnames,tsyn)
-	    val (thy',typedef_info) = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy	    
+	    val (typedef_info, thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy	    
             val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
 				      
 	    val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
@@ -2187,7 +2187,7 @@
 	    val tnames = sort string_ord (map fst tfrees)
 	    val tsyn = mk_syn thy tycname
 	    val typ = (tycname,tnames,tsyn)
-	    val (thy', typedef_info) = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
+	    val (typedef_info, thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
 	    val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
 	    val fulltyname = Sign.intern_type thy' tycname
 	    val aty = Type (fulltyname, map mk_vartype tnames)
diff -r f2283f334e42 -r 36e537f89585 src/HOL/Import/replay.ML
--- a/src/HOL/Import/replay.ML	Thu Apr 06 16:12:57 2006 +0200
+++ b/src/HOL/Import/replay.ML	Thu Apr 06 16:13:17 2006 +0200
@@ -344,7 +344,7 @@
 	  | delta (Hol_theorem (thyname, thmname, th)) thy =
 	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
 	  | delta (Typedef (thmname, typ, c, repabs, th)) thy = 
-	    fst(TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
+	    snd (TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
 	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
 	    add_hol4_type_mapping thyname tycname true fulltyname thy
 	  | delta (Indexed_theorem (i, th)) thy = 
diff -r f2283f334e42 -r 36e537f89585 src/HOLCF/IOA/Modelcheck/MuIOA.ML
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Thu Apr 06 16:12:57 2006 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Thu Apr 06 16:13:17 2006 +0200
@@ -157,14 +157,12 @@
 
 in
 
-fun mk_sim_oracle sign (subgoal,thl) =
-(let
-        val weak_case_congs = DatatypePackage.weak_case_congs_of sign;
-
-	val concl = (Logic.strip_imp_concl subgoal);
-
-	val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
-	val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl));
+fun mk_sim_oracle sign (subgoal, thl) = (
+  let
+    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
+    val concl = Logic.strip_imp_concl subgoal;
+    val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
+    val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl));
 	val sc_str = delete_ul_string(Sign.string_of_term sign (StartC sign concl));	
 	val sa_str = delete_ul_string(Sign.string_of_term sign (StartA sign concl));
 	val tc_str = delete_ul_string(Sign.string_of_term sign (TransC sign concl));
diff -r f2283f334e42 -r 36e537f89585 src/HOLCF/pcpodef_package.ML
--- a/src/HOLCF/pcpodef_package.ML	Thu Apr 06 16:12:57 2006 +0200
+++ b/src/HOLCF/pcpodef_package.ML	Thu Apr 06 16:13:17 2006 +0200
@@ -98,14 +98,13 @@
     fun make_po tac thy =
       thy
       |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
-      |>> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
+      ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
            (ClassPackage.intro_classes_tac [])
-      |>>> (PureThy.add_defs_i true [Thm.no_attributes less_def] #> Library.swap)
-      |> (fn (thy', ({type_definition, set_def, ...}, [less_definition])) =>
-           thy'
-           |> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
+      ||>> PureThy.add_defs_i true [Thm.no_attributes less_def]
+      |-> (fn ({type_definition, set_def, ...}, [less_definition]) =>
+          AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
              (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)
-           |> rpair (type_definition, less_definition, set_def));
+           #> rpair (type_definition, less_definition, set_def));
     
     fun make_cpo admissible (theory, defs as (type_def, less_def, set_def)) =
       let