adapted to new PureThy.add_thms etc.;
authorwenzelm
Mon Mar 13 13:16:57 2000 +0100 (2000-03-13)
changeset 8428be4c8a57cf7e
parent 8427 b19b817522a5
child 8429 515fa7533354
adapted to new PureThy.add_thms etc.;
src/HOL/Tools/record_package.ML
src/HOL/Tools/typedef_package.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Mon Mar 13 13:16:43 2000 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Mon Mar 13 13:16:57 2000 +0100
     1.3 @@ -56,8 +56,6 @@
     1.4  val (op :==) = Logic.mk_defpair;
     1.5  val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq;
     1.6  
     1.7 -fun get_defs thy specs = map (PureThy.get_thm thy o fst) specs;
     1.8 -
     1.9  
    1.10  (* proof by simplification *)
    1.11  
    1.12 @@ -613,15 +611,11 @@
    1.13  
    1.14      (* 2nd stage: defs_thy *)
    1.15  
    1.16 -    val defs_thy =
    1.17 +    val (defs_thy, (field_defs, dest_defs)) =
    1.18        types_thy
    1.19 -       |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base))
    1.20 -         (field_decls @ dest_decls)
    1.21 -       |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal])))
    1.22 -         (field_specs @ dest_specs);
    1.23 -
    1.24 -    val field_defs = get_defs defs_thy field_specs;
    1.25 -    val dest_defs = get_defs defs_thy dest_specs;
    1.26 +       |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls)
    1.27 +       |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) field_specs
    1.28 +       |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) dest_specs;
    1.29  
    1.30  
    1.31      (* 3rd stage: thms_thy *)
    1.32 @@ -639,7 +633,7 @@
    1.33  
    1.34      val thms_thy =
    1.35        defs_thy
    1.36 -      |> (PureThy.add_thmss o map Thm.no_attributes)
    1.37 +      |> (#1 oo (PureThy.add_thmss o map Thm.no_attributes))
    1.38          [("field_defs", field_defs),
    1.39            ("dest_defs", dest_defs),
    1.40            ("dest_convs", dest_convs),
    1.41 @@ -782,7 +776,7 @@
    1.42  
    1.43      (* 2nd stage: defs_thy *)
    1.44  
    1.45 -    val defs_thy =
    1.46 +    val (defs_thy, ((sel_defs, update_defs), make_defs)) =
    1.47        fields_thy
    1.48        |> Theory.parent_path
    1.49        |> Theory.add_tyabbrs_i recordT_specs     (*not made part of record name space!*)
    1.50 @@ -790,13 +784,9 @@
    1.51        |> Theory.add_trfuns ([], [], field_tr's, [])
    1.52        |> (Theory.add_consts_i o map Syntax.no_syn)
    1.53          (sel_decls @ update_decls @ make_decls)
    1.54 -      |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal])))
    1.55 -        (sel_specs @ update_specs)
    1.56 -      |> (PureThy.add_defs_i o map Thm.no_attributes) make_specs;
    1.57 -
    1.58 -    val sel_defs = get_defs defs_thy sel_specs;
    1.59 -    val update_defs = get_defs defs_thy update_specs;
    1.60 -    val make_defs = get_defs defs_thy make_specs;
    1.61 +      |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) sel_specs
    1.62 +      |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) update_specs
    1.63 +      |>>> (PureThy.add_defs_i o map Thm.no_attributes) make_specs;
    1.64  
    1.65  
    1.66      (* 3rd stage: thms_thy *)
    1.67 @@ -812,13 +802,13 @@
    1.68  
    1.69      val thms_thy =
    1.70        defs_thy
    1.71 -      |> (PureThy.add_thmss o map Thm.no_attributes)
    1.72 +      |> (#1 oo (PureThy.add_thmss o map Thm.no_attributes))
    1.73          [("select_defs", sel_defs),
    1.74            ("update_defs", update_defs),
    1.75            ("make_defs", make_defs),
    1.76            ("select_convs", sel_convs),
    1.77            ("update_convs", update_convs)]
    1.78 -      |> PureThy.add_thmss
    1.79 +      |> (#1 oo PureThy.add_thmss)
    1.80          [(("simps", simps), [Simplifier.simp_add_global]),
    1.81           (("iffs", iffs), [iff_add_global])];
    1.82  
     2.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Mar 13 13:16:43 2000 +0100
     2.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Mar 13 13:16:57 2000 +0100
     2.3 @@ -140,9 +140,9 @@
     2.4         ((if no_def then [] else [(name, setT, NoSyn)]) @
     2.5          [(Rep_name, newT --> oldT, NoSyn),
     2.6           (Abs_name, oldT --> newT, NoSyn)])
     2.7 -      |> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes)
     2.8 +      |> (if no_def then I else (#1 oo (PureThy.add_defs_i o map Thm.no_attributes))
     2.9         [Logic.mk_defpair (setC, set)])
    2.10 -      |> (PureThy.add_axioms_i o map Thm.no_attributes)
    2.11 +      |> (#1 oo (PureThy.add_axioms_i o map Thm.no_attributes))
    2.12         [(Rep_name, rep_type),
    2.13          (Rep_name ^ "_inverse", rep_type_inv),
    2.14          (Abs_name ^ "_inverse", abs_type_inv)]
     3.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Mar 13 13:16:43 2000 +0100
     3.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Mar 13 13:16:57 2000 +0100
     3.3 @@ -216,10 +216,10 @@
     3.4  fun add_axms f args thy =
     3.5    f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
     3.6  
     3.7 -val add_axioms = add_axms PureThy.add_axioms o map Comment.ignore;
     3.8 -val add_axioms_i = PureThy.add_axioms_i o map Comment.ignore;
     3.9 -val add_defs = add_axms PureThy.add_defs o map Comment.ignore;
    3.10 -val add_defs_i = PureThy.add_defs_i o map Comment.ignore;
    3.11 +val add_axioms = add_axms (#1 oo PureThy.add_axioms) o map Comment.ignore;
    3.12 +val add_axioms_i = (#1 oo PureThy.add_axioms_i) o map Comment.ignore;
    3.13 +val add_defs = add_axms (#1 oo PureThy.add_defs) o map Comment.ignore;
    3.14 +val add_defs_i = (#1 oo PureThy.add_defs_i) o map Comment.ignore;
    3.15  
    3.16  
    3.17  (* constdefs *)