--- 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)
--- 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;
--- 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)
--- 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 =
--- 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));
--- 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