# HG changeset patch
# User wenzelm
# Date 953163382 -3600
# Node ID 82826ed95d4ba13837491bff08ac7b93f1706d27
# Parent  6e0f23304061d87718da70852f22b35d01665de5
Splitter support;

diff -r 6e0f23304061 -r 82826ed95d4b src/HOL/Isar_examples/W_correct.thy
--- a/src/HOL/Isar_examples/W_correct.thy	Thu Mar 16 00:35:27 2000 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy	Thu Mar 16 00:36:22 2000 +0100
@@ -90,13 +90,6 @@
 
 subsection {* Correctness theorem *};
 
-text_raw {* \begin{comment} *};
-
-(* FIXME proper split att/mod *)
-ML_setup {* Addsplits [split_bind]; *};
-
-text_raw {* \end{comment} *};
-
 theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t";
 proof -;
   assume W_ok: "W e a n = Ok (s, t, m)";
@@ -112,7 +105,7 @@
       assume "Ok (s, t, m) = W (Abs e) a n";
       thus "$ s a |- Abs e :: t";
 	obtain t' where "t = s n -> t'" "Ok (s, t', m) = W e (TVar n # a) (Suc n)";
-	  by (rule rev_mp) simp;
+	  by (rule rev_mp) (simp split: split_bind);
 	with hyp; show ?thesis; by (force intro: has_type.Abs);
       qed;
     qed;
@@ -128,7 +121,7 @@
           and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
           and W1_ok: "W e1 a n = Ok (s1, t1, n1)"
           and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)";
-	    by (rule rev_mp) simp;
+	    by (rule rev_mp) (simp split: split_bind);
         show ?thesis;
         proof (rule has_type.App);
           from s; have s': "$ u ($ s2 ($ s1 a)) = $s a";