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