1.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML Mon Jun 16 17:56:08 2008 +0200
1.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Mon Jun 16 22:13:39 2008 +0200
1.3 @@ -376,7 +376,7 @@
1.4 val goal = lift_defined %: (nonlazy args, concl);
1.5 fun tacs ctxt = [
1.6 rtac @{thm rev_contrapos} 1,
1.7 - RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
1.8 + eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
1.9 asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
1.10 in pg [] goal tacs end;
1.11 in
1.12 @@ -477,7 +477,7 @@
1.13 mk_trp (con_app con1 args1 ~<< con_app con2 args2));
1.14 fun tacs ctxt = [
1.15 rtac @{thm rev_contrapos} 1,
1.16 - RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
1.17 + eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
1.18 @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2)
1.19 @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
1.20 in pg [] goal tacs end;
1.21 @@ -709,7 +709,7 @@
1.22 mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
1.23 val take_ss = HOL_ss addsimps take_rews;
1.24 fun quant_tac ctxt i = EVERY
1.25 - (mapn (fn n => fn _ => RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
1.26 + (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
1.27
1.28 fun ind_prems_tac prems = EVERY
1.29 (maps (fn cons =>
1.30 @@ -766,7 +766,7 @@
1.31 map (K (atac 1)) (nonlazy args) @
1.32 map (K (etac spec 1)) (List.filter is_rec args);
1.33 fun cases_tacs (cons, cases) =
1.34 - RuleInsts.res_inst_tac context [(("x", 0), "x")] cases 1 ::
1.35 + res_inst_tac context [(("x", 0), "x")] cases 1 ::
1.36 asm_simp_tac (take_ss addsimps prems) 1 ::
1.37 maps con_tacs cons;
1.38 in
1.39 @@ -783,8 +783,8 @@
1.40 val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
1.41 val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
1.42 fun tacf {prems, context} = [
1.43 - RuleInsts.res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1,
1.44 - RuleInsts.res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
1.45 + res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1,
1.46 + res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
1.47 stac fix_def2 1,
1.48 REPEAT (CHANGED
1.49 (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
1.50 @@ -833,7 +833,7 @@
1.51 val goal =
1.52 mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
1.53 fun arg_tacs ctxt vn = [
1.54 - RuleInsts.eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
1.55 + eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
1.56 etac disjE 1,
1.57 asm_simp_tac (HOL_ss addsimps con_rews) 1,
1.58 asm_simp_tac take_ss 1];
1.59 @@ -843,7 +843,7 @@
1.60 fun foo_tacs ctxt n (cons, cases) =
1.61 simp_tac take_ss 1 ::
1.62 rtac allI 1 ::
1.63 - RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
1.64 + res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
1.65 asm_simp_tac take_ss 1 ::
1.66 maps (con_tacs ctxt) cons;
1.67 fun tacs ctxt =
1.68 @@ -887,8 +887,7 @@
1.69 else (* infinite case *)
1.70 let
1.71 fun one_finite n dn =
1.72 - RuleInsts.read_instantiate global_ctxt
1.73 - [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
1.74 + read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
1.75 val finites = mapn one_finite 1 dnames;
1.76
1.77 val goal =
1.78 @@ -936,7 +935,7 @@
1.79 fun x_tacs ctxt n x = [
1.80 rotate_tac (n+1) 1,
1.81 etac all2E 1,
1.82 - RuleInsts.eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
1.83 + eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
1.84 TRY (safe_tac HOL_cs),
1.85 REPEAT (CHANGED (asm_simp_tac take_ss 1))];
1.86 fun tacs ctxt = [