src/HOL/Tools/res_atp_setup.ML

--- a/src/HOL/Tools/res_atp_setup.ML	Wed Oct 04 14:14:33 2006 +0200
+++ b/src/HOL/Tools/res_atp_setup.ML	Wed Oct 04 14:17:38 2006 +0200
@@ -180,13 +180,13 @@
 exception FN_LG of term;
 
 fun fn_lg (t as Const(f,tp)) (lg,seen) = 
-    if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
+    if has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
   | fn_lg (t as Free(f,tp)) (lg,seen) = 
-    if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
+    if has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
   | fn_lg (t as Var(f,tp)) (lg,seen) =
-    if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg,t ins seen)
-    else (lg,t ins seen)
-  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
+    if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen)
+    else (lg, insert (op =) t seen)
+  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg, insert (op =) t seen)
   | fn_lg f _ = raise FN_LG(f); 
 
 
@@ -204,10 +204,10 @@
 exception PRED_LG of term;
 
 fun pred_lg (t as Const(P,tp)) (lg,seen)= 
-    if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
+    if has_bool_arg tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
   | pred_lg (t as Free(P,tp)) (lg,seen) =
-    if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
-  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
+    if has_bool_arg tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen)
+  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
   | pred_lg P _ = raise PRED_LG(P);