# HG changeset patch
# User blanchet
# Date 1302773045 -7200
# Node ID be52d9bed9f63702c1475d14112aaee1b45b4373
# Parent  5ecd559936067b7f85816851c8236eaa50fba2f4
remove experimental code added in 85bb6fbb8e6a

diff -r 5ecd55993606 -r be52d9bed9f6 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Thu Apr 14 11:24:05 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Thu Apr 14 11:24:05 2011 +0200
@@ -14,7 +14,6 @@
   val size_of_subgoals: thm -> int
   val has_too_many_clauses: Proof.context -> term -> bool
   val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
-  val make_xxx_skolem: Proof.context -> thm list -> thm -> thm
   val finish_cnf: thm list -> thm list
   val presimplify: thm -> thm
   val make_nnf: Proof.context -> thm -> thm
@@ -394,48 +393,6 @@
 
 fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, [])
 
-val disj_imp_cong =
-  @{lemma "[| P --> P'; Q --> Q'; P | Q |] ==> P' | Q'" by auto}
-
-val impI = @{thm impI}
-
-(* ### *)
-(* Match untyped terms. *)
-fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
-  | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
-  | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = true
-  | untyped_aconv (Free (a, _)) (Var ((b, _), _)) = true
-  | untyped_aconv (Var ((a, _), _)) (Free (b, _)) = true
-  | untyped_aconv (Bound i) (Bound j) = (i = j)
-  | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
-  | untyped_aconv (t1 $ t2) (u1 $ u2) =
-    untyped_aconv t1 u1 andalso untyped_aconv t2 u2
-  | untyped_aconv _ _ = false
-
-fun make_xxx_skolem ctxt skolem_ths th =
-  let
-    val thy = ProofContext.theory_of ctxt
-    fun do_connective fwd_thm t1 t2 =
-      do_formula t1
-      COMP rotate_prems 1 (do_formula t2 COMP (rotate_prems 2 fwd_thm))
-    and do_formula t =
-      case t of
-        @{const Trueprop} $ t' => do_formula t'
-      | @{const conj} $ t1 $ t2 => do_connective @{thm conj_forward} t1 t2
-      | @{const disj} $ t1 $ t2 => do_connective @{thm disj_forward} t1 t2
-      | Const (@{const_name Ex}, _) $ Abs _ =>
-        let
-          val th =
-            find_first (fn sko_th => (untyped_aconv (Logic.nth_prem (1, prop_of sko_th)) (HOLogic.mk_Trueprop t)))
-                       skolem_ths |> the
-        in
-          th
-          RS
-          do_formula (Logic.strip_imp_concl (prop_of th))
-        end
-      | _ => Thm.trivial (cterm_of thy (HOLogic.mk_Trueprop t))
-  in th COMP do_formula (HOLogic.dest_Trueprop (prop_of th)) end
-
 (*Generalization, removal of redundant equalities, removal of tautologies.*)
 fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);