src/FOLP/simpdata.ML

--- a/src/FOLP/simpdata.ML	Wed Aug 12 16:20:49 1998 +0200
+++ b/src/FOLP/simpdata.ML	Wed Aug 12 16:21:18 1998 +0200
@@ -73,16 +73,25 @@
     | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F 
     | _ => make_iff_T th;
 
-fun atomize th = case concl_of th of (*The operator below is "Proof $ P $ p"*)
-      _ $ (Const("op -->",_) $ _ $ _) $ _ => atomize(th RS mp)
-    | _ $ (Const("op &",_) $ _ $ _) $ _ => atomize(th RS conjunct1) @
-                                       atomize(th RS conjunct2)
-    | _ $ (Const("All",_) $ _) $ _ => atomize(th RS spec)
-    | _ $ (Const("True",_)) $ _ => []
-    | _ $ (Const("False",_)) $ _ => []
-    | _ => [th];
+
+val mksimps_pairs =
+  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
+   ("All", [spec]), ("True", []), ("False", [])];
 
-fun mk_rew_rules th = map mk_eq (atomize th);
+fun mk_atomize pairs =
+  let fun atoms th =
+        (case concl_of th of
+           Const("Trueprop",_) $ p =>
+             (case head_of p of
+                Const(a,_) =>
+                  (case assoc(pairs,a) of
+                     Some(rls) => flat (map atoms ([th] RL rls))
+                   | None => [th])
+              | _ => [th])
+         | _ => [th])
+  in atoms end;
+
+fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th);
 
 (*destruct function for analysing equations*)
 fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)