src/HOLCF/domain/theorems.ML
changeset 15531 08c8dad8e399
parent 15457 1fbd4aba46e3
child 15570 8d8c70b41bab
     1.1 --- a/src/HOLCF/domain/theorems.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  (* ----- general proof facilities ------------------------------------------- *)
     1.5  
     1.6  fun inferT sg pre_tm =
     1.7 -  #1 (Sign.infer_types (Sign.pp sg) sg (K None) (K None) [] true ([pre_tm],propT));
     1.8 +  #1 (Sign.infer_types (Sign.pp sg) sg (K NONE) (K NONE) [] true ([pre_tm],propT));
     1.9  
    1.10  fun pg'' thy defs t = let val sg = sign_of thy;
    1.11                            val ct = Thm.cterm_of sg (inferT sg t);
    1.12 @@ -65,7 +65,7 @@
    1.13  
    1.14  (* ----- getting the axioms and definitions --------------------------------- *)
    1.15  
    1.16 -local fun ga s dn = get_thm thy (dn ^ "." ^ s, None) in
    1.17 +local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in
    1.18  val ax_abs_iso    = ga "abs_iso"  dname;
    1.19  val ax_rep_iso    = ga "rep_iso"  dname;
    1.20  val ax_when_def   = ga "when_def" dname;
    1.21 @@ -341,7 +341,7 @@
    1.22  
    1.23  (* ----- getting the composite axiom and definitions ------------------------ *)
    1.24  
    1.25 -local fun ga s dn = get_thm thy (dn ^ "." ^ s, None) in
    1.26 +local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in
    1.27  val axs_reach      = map (ga "reach"     ) dnames;
    1.28  val axs_take_def   = map (ga "take_def"  ) dnames;
    1.29  val axs_finite_def = map (ga "finite_def") dnames;
    1.30 @@ -349,8 +349,8 @@
    1.31  val ax_bisim_def   =      ga "bisim_def" comp_dnam;
    1.32  end; (* local *)
    1.33  
    1.34 -local fun gt  s dn = get_thm  thy (dn ^ "." ^ s, None);
    1.35 -      fun gts s dn = get_thms thy (dn ^ "." ^ s, None) in
    1.36 +local fun gt  s dn = get_thm  thy (dn ^ "." ^ s, NONE);
    1.37 +      fun gts s dn = get_thms thy (dn ^ "." ^ s, NONE) in
    1.38  val cases     =       map (gt  "casedist" ) dnames;
    1.39  val con_rews  = flat (map (gts "con_rews" ) dnames);
    1.40  val copy_rews = flat (map (gts "copy_rews") dnames);