# HG changeset patch
# User wenzelm
# Date 1185712191 -7200
# Node ID 0a41d2ebc0cdf4da0004d861a6ecfa21372d98c7
# Parent  936cc23a34727b9e62ebeced5c5c69074a5838e2
proper simproc_setup for "list_neq";

diff -r 936cc23a3472 -r 0a41d2ebc0cd src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Jul 29 14:29:50 2007 +0200
+++ b/src/HOL/List.thy	Sun Jul 29 14:29:51 2007 +0200
@@ -376,16 +376,16 @@
 by (induct xs arbitrary: ys) (case_tac x, auto)+
 
 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
-apply(rule Eq_FalseI)
-by auto
-
+  by (rule Eq_FalseI) auto
+
+simproc_setup list_neq ("(xs::'a list) = ys") = {*
 (*
 Reduces xs=ys to False if xs and ys cannot be of the same length.
 This is the case if the atomic sublists of one are a submultiset
 of those of the other list and there are fewer Cons's in one than the other.
 *)
-ML_setup {*
-local
+
+let
 
 fun len (Const("List.list.Nil",_)) acc = acc
   | len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
@@ -394,8 +394,9 @@
   | len (Const("List.map",_) $ _ $ xs) acc = len xs acc
   | len t (ts,n) = (t::ts,n);
 
-fun list_eq ss (Const(_,eqT) $ lhs $ rhs) =
+fun list_neq _ ss ct =
   let
+    val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;
     val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
     fun prove_neq() =
       let
@@ -411,15 +412,7 @@
        n < m andalso submultiset (op aconv) (rs,ls)
     then prove_neq() else NONE
   end;
-
-in
-
-val list_neq_simproc =
-  Simplifier.simproc @{theory} "list_neq" ["(xs::'a list) = ys"] (K list_eq);
-
-end;
-
-Addsimprocs [list_neq_simproc];
+in list_neq end;
 *}