# HG changeset patch
# User oheimb
# Date 884277746 -3600
# Node ID b96b513c6c658890950b57bee2d1d2b69bdfe9fe
# Parent  7399288f5dd3c3e1a9d4de486b028815528c23a2
replaced  fn _ =>  by  K

diff -r 7399288f5dd3 -r b96b513c6c65 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Jan 08 16:52:31 1998 +0100
+++ b/src/HOL/simpdata.ML	Thu Jan 08 17:42:26 1998 +0100
@@ -54,7 +54,7 @@
 
 local
 
-  fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
+  fun prover s = prove_goal HOL.thy s (K [blast_tac HOL_cs 1]);
 
   val P_imp_P_iff_True = prover "P --> (P = True)" RS mp;
   val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
@@ -166,11 +166,11 @@
 
 val True_implies_equals = prove_goal HOL.thy
  "(True ==> PROP P) == PROP P"
-(fn _ => [rtac equal_intr_rule 1, atac 2,
+(K [rtac equal_intr_rule 1, atac 2,
           METAHYPS (fn prems => resolve_tac prems 1) 1,
           rtac TrueI 1]);
 
-fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [blast_tac HOL_cs 1]);
+fun prove nm thm  = qed_goal nm HOL.thy thm (K [blast_tac HOL_cs 1]);
 
 prove "conj_commute" "(P&Q) = (Q&P)";
 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
@@ -239,16 +239,16 @@
 prove "eq_sym_conv" "(x=y) = (y=x)";
 
 qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
- (fn _ => [rtac refl 1]);
+ (K [rtac refl 1]);
 
 qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
   (fn [prem] => [rewtac prem, rtac refl 1]);
 
 qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
- (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]);
+ (K [Blast_tac 1]);
 
 qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
- (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]);
+ (K [Blast_tac 1]);
 
 qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x"
  (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
@@ -257,7 +257,7 @@
  (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
 *)
 qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
- (fn _ => [blast_tac (HOL_cs addIs [select_equality]) 1]);
+ (K [Blast_tac 1]);
 
 qed_goal "expand_if" HOL.thy
     "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
@@ -273,7 +273,7 @@
 
 qed_goal "if_bool_eq" HOL.thy
                    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
-                   (fn _ => [rtac expand_if 1]);
+                   (K [rtac expand_if 1]);
 
 
 (*** make simplification procedures for quantifier elimination ***)
@@ -337,7 +337,7 @@
 
 
 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
-  (fn _ => [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
+  (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
 
 (** 'if' congruence rules: neither included by default! *)
 
@@ -395,10 +395,10 @@
 
 qed_goal "if_distrib" HOL.thy
   "f(if c then x else y) = (if c then f x else f y)" 
-  (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
+  (K [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
 
 qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
-  (fn _ => [rtac ext 1, rtac refl 1]);
+  (K [rtac ext 1, rtac refl 1]);
 
 
 (*For expand_case_tac*)