src/HOLCF/domain/theorems.ML
changeset 1674 33aff4d854e4
parent 1644 681f70ca3cf7
child 1781 cc5f55a0fbd7
     1.1 --- a/src/HOLCF/domain/theorems.ML	Tue Apr 23 16:58:57 1996 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Tue Apr 23 17:01:51 1996 +0200
     1.3 @@ -45,9 +45,9 @@
     1.4  in drep end;
     1.5  val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
     1.6  
     1.7 -local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn prems=>[rtac TrueI 1])in
     1.8 +local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in
     1.9  val kill_neq_tac = dtac trueI2 end;
    1.10 -fun case_UU_tac rews i v =	res_inst_tac [("Q",v^"=UU")] classical2 i THEN
    1.11 +fun case_UU_tac rews i v =	case_tac (v^"=UU") i THEN
    1.12  				asm_simp_tac (HOLCF_ss addsimps rews) i;
    1.13  
    1.14  val chain_tac = REPEAT_DETERM o resolve_tac