diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Recipes/external_solver.ML
--- a/CookBook/Recipes/external_solver.ML	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-signature IFF_SOLVER =
-sig
-  val decide : string -> bool
-end
-
-
-structure IffSolver : IFF_SOLVER =
-struct
-
-exception FAIL
-
-datatype formula = Atom of string | Iff of formula * formula
-
-fun scan s =
-  let
-
-    fun push yss = [] :: yss 
-
-    fun add x (ys :: yss) = (x :: ys) :: yss
-      | add _ _ = raise FAIL
-
-    fun pop ([a, b] :: yss) = add (Iff (b, a)) yss
-      | pop _ = raise FAIL
-
-    fun formula [] acc = acc
-      | formula ("(" :: xs) acc = formula xs (push acc)
-      | formula (")" :: xs) acc = formula xs (pop acc)
-      | formula ("<=>" :: xs) acc = formula xs acc
-      | formula (x :: xs) acc = formula xs (add (Atom x) acc)
-
-    val tokens = String.tokens (fn c => c = #" ") s
-  in
-    (case formula tokens [[]] of
-      [[f]] => f
-    | _ => raise FAIL)
-  end
-
-
-fun decide s =
-  let
-    fun fold_atoms f (Atom n) = f s
-      | fold_atoms f (Iff (p, q)) = fold_atoms f p #> fold_atoms f q
-
-    fun collect s tab =
-      (case Symtab.lookup tab s of
-        NONE => Symtab.update (s, false) tab
-      | SOME v => Symtab.update (s, not v) tab)
-
-    fun check tab = Symtab.fold (fn (_, v) => fn b => b andalso v) tab true
-  in 
-    (case try scan s of
-      NONE => false
-    | SOME f => check (fold_atoms collect f Symtab.empty))
-  end
-
-end