--- a/src/HOLCF/domain/theorems.ML Wed Nov 30 00:59:04 2005 +0100
+++ b/src/HOLCF/domain/theorems.ML Wed Nov 30 01:01:15 2005 +0100
@@ -209,18 +209,19 @@
val pat_rews = let
fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
- fun pat_lhs (con,args) = list_comb (%%:(pat_name con), ps args);
- fun pat_rhs (con,[]) = %%:returnN ` (%:"rhs")
- | pat_rhs (con,args) = (foldr1 cpair_pat (ps args))`(%:"rhs")`(mk_ctuple (map %# args));
- val pat_stricts = map (fn (con,args) => pg axs_pat_def (mk_trp(
- strict(pat_lhs (con,args)`(%:"rhs"))))
- [simp_tac (HOLCF_ss addsimps [when_strict]) 1]) cons;
- val pat_apps = let fun one_pat c (con,args)= pg axs_pat_def
+ fun pat_lhs (con,args) = %%:branchN $ list_comb (%%:(pat_name con), ps args);
+ fun pat_rhs (con,[]) = %%:returnN ` ((%:"rhs") ` HOLogic.unit)
+ | pat_rhs (con,args) =
+ (%%:branchN $ foldr1 cpair_pat (ps args))`(%:"rhs")`(mk_ctuple (map %# args));
+ val pat_stricts = map (fn (con,args) => pg (branch_def::axs_pat_def)
+ (mk_trp(strict(pat_lhs (con,args)`(%:"rhs"))))
+ [simp_tac (HOLCF_ss addsimps [when_strict]) 1]) cons;
+ val pat_apps = let fun one_pat c (con,args) = pg (branch_def::axs_pat_def)
(lift_defined %: (nonlazy args,
(mk_trp((pat_lhs c)`(%:"rhs")`(con_app con args) ===
(if con = fst c then pat_rhs c else %%:failN)))))
[asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in List.concat(map (fn c => map (one_pat c) cons) cons) end;
+ in List.concat (map (fn c => map (one_pat c) cons) cons) end;
in pat_stricts @ pat_apps end;
val con_stricts = List.concat(map (fn (con,args) => map (fn vn =>
@@ -369,7 +370,7 @@
("copy_rews", copy_rews)])))
|> (#1 o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])])
|> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
- dist_les @ dist_eqs @ copy_rews)
+ pat_rews @ dist_les @ dist_eqs @ copy_rews)
end; (* let *)
fun comp_theorems (comp_dnam, eqs: eq list) thy =