src/Pure/pure_thy.ML
changeset 11516 a0633bdcd015
parent 10667 75a1c9575edb
child 11631 b325c05709d3
     1.1 --- a/src/Pure/pure_thy.ML	Fri Aug 31 16:10:03 2001 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Fri Aug 31 16:11:20 2001 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4    val thms_containing: theory -> string list -> (string * thm) list
     1.5    val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
     1.6    val smart_store_thms: (bstring * thm list) -> thm list
     1.7 +  val open_smart_store_thms: (bstring * thm list) -> thm list
     1.8    val forall_elim_var: int -> thm -> thm
     1.9    val forall_elim_vars: int -> thm -> thm
    1.10    val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list
    1.11 @@ -234,11 +235,11 @@
    1.12  fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
    1.13  fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
    1.14  
    1.15 -fun enter_thmx _ app_name ("", thmx) = map #2 (app_name "" thmx)
    1.16 -  | enter_thmx sg app_name (bname, thmx) =
    1.17 +fun enter_thmx _ _ app_name ("", thmx) = map snd (app_name "" thmx)
    1.18 +  | enter_thmx sg name_thm app_name (bname, thmx) =
    1.19        let
    1.20          val name = Sign.full_name sg bname;
    1.21 -        val named_thms = map Thm.name_thm (app_name name thmx);
    1.22 +        val named_thms = map name_thm (app_name name thmx);
    1.23  
    1.24          val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg;
    1.25  
    1.26 @@ -262,7 +263,7 @@
    1.27  fun add_thmx app_name app_att ((bname, thmx), atts) thy =
    1.28    let
    1.29      val (thy', thmx') = app_att ((thy, thmx), atts);
    1.30 -    val thms'' = enter_thmx (Theory.sign_of thy') app_name (bname, thmx');
    1.31 +    val thms'' = enter_thmx (Theory.sign_of thy') Thm.name_thm app_name (bname, thmx');
    1.32    in (thy', thms'') end;
    1.33  
    1.34  fun add_thms args theory =
    1.35 @@ -284,7 +285,7 @@
    1.36        val (thy', thmss') =
    1.37          foldl_map app (thy, map (fn (ths, atts) => (ths, atts @ more_atts @ kind_atts)) ths_atts);
    1.38        val thms' = flat thmss';
    1.39 -      val thms'' = enter_thmx (Theory.sign_of thy') name_multi (bname, thms');
    1.40 +      val thms'' = enter_thmx (Theory.sign_of thy') Thm.name_thm name_multi (bname, thms');
    1.41      in (thy', (bname, thms'')) end;
    1.42  in
    1.43    fun have_thmss kind_atts args thy = foldl_map (have_thss kind_atts) (thy, args);
    1.44 @@ -300,13 +301,18 @@
    1.45  
    1.46  (* smart_store_thms *)
    1.47  
    1.48 -fun smart_store_thms (name, []) = error ("Cannot store empty list of theorems: " ^ quote name)
    1.49 -  | smart_store_thms (name, [thm]) = enter_thmx (Thm.sign_of_thm thm) name_single (name, thm)
    1.50 -  | smart_store_thms (name, thms) =
    1.51 +fun gen_smart_store_thms _ (name, []) =
    1.52 +      error ("Cannot store empty list of theorems: " ^ quote name)
    1.53 +  | gen_smart_store_thms name_thm (name, [thm]) =
    1.54 +      enter_thmx (Thm.sign_of_thm thm) name_thm name_single (name, thm)
    1.55 +  | gen_smart_store_thms name_thm (name, thms) =
    1.56        let
    1.57          val merge_sg = Sign.merge_refs o apsnd (Sign.self_ref o Thm.sign_of_thm);
    1.58          val sg_ref = foldl merge_sg (Sign.self_ref (Thm.sign_of_thm (hd thms)), tl thms);
    1.59 -      in enter_thmx (Sign.deref sg_ref) name_multi (name, thms) end;
    1.60 +      in enter_thmx (Sign.deref sg_ref) name_thm name_multi (name, thms) end;
    1.61 +
    1.62 +val smart_store_thms = gen_smart_store_thms Thm.name_thm;
    1.63 +val open_smart_store_thms = gen_smart_store_thms snd;
    1.64  
    1.65  
    1.66  (* forall_elim_vars (belongs to drule.ML) *)
    1.67 @@ -446,7 +452,7 @@
    1.68  
    1.69  val proto_pure =
    1.70    Theory.pre_pure
    1.71 -  |> Library.apply [TheoremsData.init, TheoryManagementData.init]
    1.72 +  |> Library.apply [TheoremsData.init, TheoryManagementData.init, Proofterm.init]
    1.73    |> put_name "ProtoPure"
    1.74    |> global_path
    1.75    |> Theory.add_types
    1.76 @@ -486,6 +492,7 @@
    1.77    |> (#1 oo (add_defs_i false o map Thm.no_attributes))
    1.78     [("Goal_def", let val A = Free ("A", propT) in Logic.mk_equals (Logic.mk_goal A, A) end)]
    1.79    |> (#1 o add_thmss [(("nothing", []), [])])
    1.80 +  |> Theory.add_axioms_i Proofterm.equality_axms
    1.81    |> end_theory;
    1.82  
    1.83  structure ProtoPure =